%This is a copy of freiburg.bib made on 2.2.12 

@PREAMBLE{"\newcommand{\SortNoop}[1]{}"}
%Mind all the curly brackets when this is used! They are important!
@STRING{ lncs = "{LNCS}" }
@STRING{ ngc = "New {G}eneration {C}omputing" }
@STRING{ entcs = "Electronic {N}otes in {T}heoretical {C}omputer {S}cience" }
@STRING{ jlp = "Journal of {L}ogic {P}rogramming" }
@STRING{ mp = "The {MIT} {P}ress" }
@STRING{ tplp = "{T}heory and {P}ractice of {L}ogic {P}rogramming" }



@InProceedings{AbrBecFraHerSch06,
  author = 	 {Erika {\'A}brah{\'a}m and Bernd Becker and Martin Fr{\"a}nzle
                  and Christian Herde and Tobias Schubert},
  title = 	 {Parallel {SAT}-Solving in Bounded Model
  Checking},
  booktitle = 	 {Proceedings of the 5th International Workshop on 
                  Parallel and Distributed Methods in verifi{C}ation},
  year =	 2006,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{AbrBecKlaSte05,
  author = 	 {Erika {\'A}brah{\'a}m and Bernd Becker and Felix Klaedtke
                  and Martin Steffen},
  title = 	 {Optimizing Bounded Model Checking for Linear Hybrid Systems},
  booktitle = 	 {Proceedings of the 6th International Conference on 
                  Verification, Model Checking, and Abstract Interpretation},
  pages =	 {396-412},
  year =	 2005,
  editor =	 {Radhia Cousot},
  volume =	 3385,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag},
  notes =        {My comments are based on a draft version.}
}

@inproceedings{AffeldtTM07,
  author    = {Reynald Affeldt and
               Miki Tanaka and
               Nicolas Marti},
  title     = {Formal Proof of Provable Security by Game-Playing in a Proof
               Assistant},
  booktitle = {ProvSec},
  year      = {2007},
  pages     = {151-168},
  ee        = {http://dx.doi.org/10.1007/978-3-540-75670-5_10},
  crossref  = {DBLP:conf/provsec/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/provsec/2007,
  editor    = {Willy Susilo and
               Joseph K. Liu and
               Yi Mu},
  title     = {Provable Security, First International Conference, ProvSec
               2007, Wollongong, Australia, November 1-2, 2007, Proceedings},
  booktitle = {ProvSec},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4784},
  year      = {2007},
  isbn      = {978-3-540-75669-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{AlfHen01,
  author = 	 {{\SortNoop{Alfaro}}de Alfaro, Luca  and Henzinger, Thomas A.},
  title = 	 {Interface automata},
  booktitle = 	 {Proceedings of ESEC / SIGSOFT
FSE},
  pages =	 {109-120},
  year =	 2001
}

@inproceedings{AlfaroHS02,
  author    = {Luca de Alfaro and
               Thomas A. Henzinger and
               Mari{\"e}lle Stoelinga},
  title     = {Timed Interfaces},
  booktitle = {EMSOFT},
  year      = {2002},
  pages     = {108-122},
  ee        = {http://dx.doi.org/10.1007/3-540-45828-X_9},
  crossref  = {DBLP:conf/emsoft/2002},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/emsoft/2002,
  editor    = {Alberto L. Sangiovanni-Vincentelli and
               Joseph Sifakis},
  title     = {Embedded Software, Second International Conference, EMSOFT
               2002, Grenoble, France, October 7-9, 2002, Proceedings},
  booktitle = {EMSOFT},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2491},
  year      = {2002},
  isbn      = {3-540-44307-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@InProceedings{AljHerLeu05,
  title =        {Counterexamples for Timed Probabilistic
                  Reachability},
  year =         {2005},
  author =       {Husain Aljazzar and Holger Hermanns and Stefan Leue},
  series =       {LNCS},
  volume =       {3829},
  pages =        {177--195},
  booktitle =    {Proceedings of the  3rd
                  International Conference on Formal Modeling and Analysis of Timed System},
  editor =       {Paul Pettersson and Wang Yi},
  publisher =    {Springer-Verlag}
}

@inproceedings{AljLeu06,
  author    = {Husain Aljazzar and
               Stefan Leue},
  editor    = {Eugene Asarin and
               Patricia Bouyer},
  title     = {Extended Directed Search for Probabilistic Timed Reachability},
  booktitle = {Proceedings of the 4th International
               Conference on Formal Modeling and Analysis of Timed Systems},
  year      = {2006},
  pages     = {33-51},  
  publisher = {Springer-Verlag},
  series    = {LNCS}, 
  volume    = {4202}
}

%"2002 IEEE/ACM International\ldots" das muss so sein.
@inproceedings{AloRamMarSak02,
  author    = {Fadi A. Aloul and
               Arathi Ramani and
               Igor L. Markov and
               Karem A. Sakallah},
  title     = {Generic {ILP} versus specialized 0-1 {ILP}: an update.},
  booktitle = {Proceedings of the 2002 IEEE/ACM International Conference
               on Computer-Aided Design},
  editor    = {Lawrence T. Pileggi and
               Andreas Kuehlmann},
  year      = {2002},
  pages     = {450-457},
  publisher = {ACM}
}

@Article{AluCouHalHenHoNicOliSifYov95,
  author = 	 {R. Alur and C. Courcoubetis and N. Halbwachs and 
                  T.A. Henzinger and P.-H. Ho and X. Nicollin and 
                  A. Olivero and J. Sifakis and S. Yovine},
  title = 	 {The Algorithmic Analysis of Hybrid Systems},
  journal = 	 {Theoretical Computer Science},
  year = 	 1995,
  volume =	 138,
  number =	 1,
  pages =	 {3-34}
}

@InProceedings{AluCouHenHo93,
  author    = {Rajeev Alur and Costas Courcoubetis and Thomas
               A. Henzinger and Pei-Hsin Ho}, 
  editor    = {Robert L. Grossman and
               Anil Nerode and
               Anders P. Ravn and
               Hans Rischel},
  title     = {Hybrid Automata: An Algorithmic Approach to the
               Specification and Verification of Hybrid Systems},
  booktitle = {Proceedings of the 1992 Hybrid Systems Conference},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {736},
  year      = {1993},
  pages     = {209-229}
}

@Article{AluDanIva06,
  author = 	 {Rajeev Alur and Thao Dang and Franjo Ivan\v{c}i{\'c}},
  title = 	 {Predicate Abstraction for Reachability Analysis of Hybrid Systems},
  journal = 	 {ACM Transactions on Embedded Computing Systems},
  year = 	 2006,
  volume =	 5,
  number =	 1,
  pages =	 {152-199}
}

@Article{AluDil94,
  author = 	 {Rajeev Alur and David L. Dill},
  title = 	 {A Theory of Timed Automata},
  journal = 	 {Theoretical Computer Science},
  year = 	 1994,
  volume =	 126,
  number =	 2,
  pages =	 {183-235}
}

@Article{AluHenHo96,
  author = 	 {Rajeev Alur and Thomas A. Henzinger and Pei-Hsin Ho},
  title = 	 {Automatic symbolic verification of embedded systems},
  journal = 	 {IEEE Transactions on Software Engineering},
  year = 	 1996,
  volume =	 22,
  pages =	 {181-201}
}

@Article{AluFixHen99,
  author = 	 {Rajeev Alur, Limor Fix, Thomas A. Henzinger},
  title = 	 {Event-Clock Automata: A Determinizable Class of Timed Automata},
  journal = 	 {Theor. Comput. Sci.},
  year = 	 1999,
  volume =	 211,
  number =	 {1-2},
  pages =	 {253-273}
}

@TechReport{AmaLevSriWin63,
  author = 	 {Amarel, S. and Levy, S. Y. and Srinivasan, C. V. and
                  Winder, R.O.},
  title = 	 {Theory Of Adjustable Switching Networks},
  institution =  {David Sarnoff Research Center Princeton NJ},
  year = 	 1963,
  number =	 {AD0435549}
}

@InProceedings{AmlMcM04,
  author = 	 {Nina Amla and Kenneth L. McMillan},
  title = 	 {A Hybrid of Counterexample-Based and Proof-Based
                  Abstraction},
  booktitle = 	 {Proceedings of the 5th International Conference on 
                  Formal Methods in Computer-Aided Design},
  pages =	 {260-274},
  year =	 2004,
  editor =	 {Alan J. Hu and Andrew K. Martin},
  volume =	 3312,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@inproceedings{AngGebLinBeuSch05,
  author    = {Christian Anger and
               Martin Gebser and
               Thomas Linke and
               Andr{\'e} Neumann and
               Torsten Schaub},
  title     = {The nomore++ Approach to Answer Set Solving},
  editor    = {Geoff Sutcliffe and
               Andrei Voronkov},
  booktitle = {Proceeding of the 12th International Conference on 
               Logic for Programming, Artificial Intelligence, and Reasoning},
  year      = {2005},
  pages     = {95-109},
  series    = {LNCS},
  volume    = {3835},
  publisher = {Springer-Verlag}
}

@InProceedings{Ang04,
  author = 	 {Nicos Angelopoulos},
  title = 	 {Upsh: A {Unix} to {Prolog} Shell},
  booktitle = 	 {Proceedings of 14th Workshop on Logic Programming
                  Environments and 3rd Workshop on Multiparadigm
                  Constraint Programming},
  pages =        {7-18},
  year =	 2004,
  editor =	 {Susana Mu{\~n}oz-Hern{\'a}ndez and Jos{\'e} Manuel G{\'o}mez-Perez
                  and Petra Hofstedt},
  note =	 {Held in conjunction with ICLP04}
}

@TechReport{Ant02,
  author = 	 {Martin Anthony},
  title = 	 {Decision Lists and Threshold Decision Lists},
  institution =  {CDAM},
  year = 	 2002,
  type =	 {Research Report},
  number =	 {LSE-CDAM-2002-11}
}

@InProceedings{AE93,
  author = 	 {K.~R.~Apt and S.~Etalle},
  editor =       {A.~Borzyszkowski and S.~Sokolowski},
  title = 	 {On the unification free {P}rolog programs},
  booktitle = 	 {Proceedings of the 18th International Symposium on 
                  Mathematical Foundations of Computer Science},
  series =	 {LNCS},
  year =	 1993,
  publisher =	 {Springer-Verlag},
  Optaddress =	 {Berlin},
  pages =	 {1--19},
  volume =       {711}
}

@InProceedings{AL95,
  author = 	 {K.~R.~Apt and I.~Luitjes},
  title = 	 {Verification of logic programs with delay declarations},
  booktitle = 	 {Proceedings of the 4th International Conference on
                     Algebraic Methodology and Software Technology},
  series =	 {LNCS},
  volume =       {936},
  year =	 1995,
  editor =       {V.~S.~Alagar and M.~Nivat},
  publisher =	 {Springer-Verlag},
  Optaddress =	 {Berlin},
  pages =        {66--90}, 
  note =	 {Invited Lecture}
}

@article{ArcherHR02,
  author    = {Myla Archer and
               Constance L. Heitmeyer and
               Elvinia Riccobene},
  title     = {Proving Invariants of {I/O} Automata with TAME},
  journal   = {Autom. Softw. Eng.},
  volume    = {9},
  number    = {3},
  year      = {2002},
  pages     = {201-232},
  ee        = {http://dx.doi.org/10.1023/A:1016320523091},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@TechReport{ArcherHRunknown,
  author = 	 {Myla Archer and
               Constance L. Heitmeyer and
               Elvinia Riccobene},
  title = 	 {Applying TAME to {I/O} Automata:
A User's Perspective},
  institution =  {US Navy},
  year = 	 {?},
  number =	 {NRL Release Number 00-1221.1-0443}
}

@InBook{BaaNut03,
  author =	 {Franz Baader and Werner Nutt},
  title = 	 {The Description Logic Handbook},
  chapter = 	 {Basic Description Logics},
  publisher = 	 {Cambridge University Press},
  year = 	 2003,
  pages =	 {43-78},
  note =	 {In \cite{BaaCalMcGNarPat03}}
}

@Book{BaaCalMcGNarPat03,
  editor =	 {Franz Baader and Diego Calvanese and Deborah
                  L. McGuinness and Daniele Nardi and Peter F. Patel-Schneider},
  title = 	 {The Description Logic Handbook: Theory, Implementation, and Applications},
  publisher = 	 {Cambridge University Press},
  year = 	 2003
}

@article{BacGan94,
  author    = {Leo Bachmair and
               Harald Ganzinger},
  title     = {Rewrite-Based Equational Theorem Proving with Selection
               and Simplification.},
  journal   = {Journal of Logic and Computation},
  volume    = {4},
  number    = {3},
  year      = {1994},
  pages     = {217-247}
}

@Book{BacWri,
  author =	 {Back and Wright},
  title = 	 {A systematic introduction},
  publisher = 	 {Publisher},
  year = 	 {}
}

@article{Bac01,
  author    = {Rolf Backofen},
  title     = {The Protein Structure Prediction Problem: A Constraint Optimization
               Approach using a New Lower Bound},
  journal   = {Constraints},
  volume    = {6},
  number    = {2/3},
  year      = {2001},
  pages     = {223-255}
}

@article{BacWilBor99,
  author    = {Rolf Backofen and
               Sebastian Will and
               Erich {Bornberg-Bauer}},
  title     = {Application of constraint programming techniques for structure
               prediction of lattice proteins with extended alphabets},
  journal   = {Bioinformatics},
  volume    = {15},
  number    = {3},
  year      = {1999},
  pages     = {234-242}
}
	
@Article{BacWil06,
  author = 	 {Rolf Backofen and Sebastian Will},
  title = 	 {A Constraint-Based Aproach to Fast and Exact Structure 
                  Prediction in Three-Dimensional Protein Models},
  journal = 	 {Constraints},
  year = 	 2006,
  volume =	 11,
  number =	 1,
  pages =	 {5-30}
}

@inproceedings{Badban1,
author = {Bahareh Badban and Martin Lange},
title = {Exact Incremental Analysis of Timed Automata with an SMT-Solver},
booktitle = {FORMATS},
year = {2011},
pages = {177-192},
editor = {Uli Fahrenberg and Stavros Tripakis},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6919},
}

@Article{BadBorStu01,
  author = 	 {Greg J. Badros and Alan Borning and Peter J. Stuckey},
  title = 	 {The {Cassowary}
                  linear arithmetic constraint solving algorithm},
  journal = 	 {ACM Transactions on Computer-Human Interaction},
  year = 	 2001,
  volume =	 8,
  number =	 4,
  pages =	 {267-306}
}

@Article{BaiBouRou06,
  author = 	 {Olivier Bailleux and Yacine Boufkhad and Olivier Roussel},
  title = 	 {A Translation of Pseudo {B}oolean Constraints to {SAT}},
  journal = 	 {Journal on Satisfiability, Boolean Modeling and Computation},
  year = 	 2006,
  volume =	 2,
  pages =	 {191-200}
}

@article{BalBocPisWol03,
  author    = {Egon Balas and
               Alexander Bockmayr and
               Nicolai Pisaruk and
               Laurence A. Wolsey},
  title     = {On Unions and Dominants of Polytopes},
  journal   = {Mathematical Programming},
  volume    = {99},
  number    = {2},
  year      = {2004},
  pages     = {223-239}
}

@inproceedings{BalMajMilRaj01,
  author    = {Thomas Ball and
               Rupak Majumdar and
               Todd D. Millstein and
               Sriram K. Rajamani},
  title     = {Automatic Predicate Abstraction of {C} Programs},
  booktitle = {Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language
               Design and Implementation},
  year      = {2001},
  pages     = {203-213},
  volume    = {36},
  number    = {5}, 
  series    = {SIGPLAN Notices}
}

@InProceedings{BalPodRaj01,
  author = 	 {Thomas Ball and Andreas Podelski and Sriram K. Rajamani},
  title = 	 {{B}oolean and {Cartesian} Abstraction for Model Checking {C} Programs},
  booktitle = 	 {Proceedings of TACAS: Tools and Algorithms for the Construction and Analysis of Systems},
  year =	 2001,
  editor =	 {Tiziana Margaria and Wang Yi},
  volume =	 2031,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag},
  pages =	 {268--283},
}

@article{BalPodRaj03,
  author    = {Thomas Ball and
               Andreas Podelski and
               Sriram K. Rajamani},
  title     = {{B}oolean and {C}artesian Abstraction for Model Checking {C} Programs},
  journal   = {International Journal on Software Tools for Technology Transfer},
  volume    = {5},
  number    = {1},
  year      = {2003},
  pages     = {49-58}
}

@Inproceedings{BalPodRaj02,
  author    = {Thomas Ball and Andreas Podelski and Sriram K. Rajamani},
  editor    = {Joost-Pieter Katoen and
               Perdita Stevens},
  booktitle = {Proceedings of the 8th International Conference on
               Tools and Algorithms for the Construction and Analysis of Systems},
  title = {Completeness of Abstraction Refinement for Software
                  Model Checking},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {2280},
  year      = {2002}
}

@inproceedings{Bar93,
  editor    = {Andrei Voronkov},
  author    = {Peter Barth},
  title     = {Linear 0-1 Inequalities and Extended Clauses},
  booktitle = {Proceedings of the 4th International Conference on 
               Logic Programming and Automated Reasoning},
  year      = {1993},
  pages     = {40-51},
  publisher = {Springer-Verlag},
  volume    = {698},
  series    = {LNCS}
}

@Book{Bar03,
  author =	 {Chitta Baral},
  title = 	 {Knowledge representation, reasoning and declarative problem solving},
  publisher = 	 {Cambridge University Press},
  year = 	 2003
}

@TechReport{Bar95,
  author = 	 {Peter Barth},
  title = 	 {A {D}avis-{P}utnam Based Enumeration Algorithm for
                  Linear Pseudo-{B}oolean Optimization},
  institution =  {Max-Planck-Institut f{\"u}s Informatik},
  year = 	 1995,
  number =	 {MPI-I-95-2-003},
  address =	 {Saarbr{\"u}cken}
}

@InProceedings{BarBoc93,
  author = 	 {Peter Barth and Alexander Bockmayr},
  title = 	 {Solving 0-1 problems in {CLP(PB)}},
  booktitle = 	 {Proceedings of the 9th Conference on Artificial
                  Intelligence for Applications},
  year =	 1993,
  organization = {IEEE}
}

@inproceedings{BasBonCri07,
  author    = {Sabrina Baselice and
               Piero A. Bonatti and
               Giovanni Criscuolo},
  title     = {On Finitely Recursive Programs},
  editor    = {Ver{\'o}nica Dahl and
               Ilkka Niemel{\"a}},
  publisher = {Springer-Verlag},
  volume    = {4670},
  series    = {LNCS},
  booktitle = {Proceedings pf the 23rd International Conference on Logic Programming},
  year      = {2007},
  pages     = {89-103}
}

@Article{BDFHF02,
  author = 	 {D. Basin and Y. Deville and P. Flener and A. Hamfelt 
                  and J. {Fischer Nilsson}},
  title = 	 {Synthesis of Programs in Computational Logic},
  journal = 	 {Theory and Practice of Logic Programming},
  year = 	 2002,
  note =	 {Accepted}
}

@Article{BFG03,
  author = 	 {D. Basin and S. Friedrich and M. Gawgowski},
  title = 	 {Bytecode Verification by Model Checking},
  journal = 	 {Kluwer???},
  year = 	 2003
}

@article{BasNic07,
  author    = {Fr{\'e}d{\'e}rique Bassino and
               Cyril Nicaud},
  title     = {Enumeration and random generation of accessible automata},
  journal   = {Theor. Comput. Sci.},
  volume    = {381},
  number    = {1-3},
  year      = {2007},
  pages     = {86-104}
}

@inproceedings{BehBouFleLar03,
  author    = {Gerd Behrmann and
               Patricia Bouyer and
               Emmanuel Fleury and
               Kim Guldstrand Larsen},
  editor    = {Hubert Garavel and
               John Hatcliff},
  title     = {Static Guard Analysis in Timed Automata Verification},
  booktitle = {Proceedings of the 9th International Conference on 
               Tools and Algorithms for the Construction and Analysis of
               Systems},
  year      = {2003},
  pages     = {254-277},
  publisher = {Springer-Verlag},
  series    = {LNCS}, 
  volume    = {2619}
}

@InProceedings{BehBenDavLarPet02,
  author = 	 {Gerd Behrmann and Johan Bengtsson and Alexandre David and Kim
                  Guldstrand Larsen and Paul Pettersson and Wang Yi},
  title = 	 {{UPPAAL} Implementation Secrets},
  booktitle = 	 {Proceedings of the 7th International Symposium on Formal Techniques in
                  Real-Time and Fault-Tolerant Systems},
  pages =	 {3-22},
  year =	 2002,
  editor =	 {Werner Damm and Ernst-R{\"u}diger Olderog},
  volume =	 2469,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Manual{BehDavLar,
  title = 	 {A Tutorial on {UPPAAL}},
  author =	 {Gerd Behrmann and Alexandre David and Kim G. Larsen},
  organization = {Department of Computer Science},
  address =	 {Aalborg, Denmark},
  note =	 {Last update 17.11.2004}
}

@inproceedings{BehDavLar04,
  author    = {Gerd Behrmann and
               Alexandre David and
               Kim Guldstrand Larsen},
  title     = {A Tutorial on {Uppaal}},
  booktitle = {Revised Lectures on Formal Methods for the Design of Real-Time Systems},
  pages     = {200-236},
  editor    = {Marco Bernardo and
               Flavio Corradini},
  series    = {LNCS},
  volume    = {3185},
  year      = {2004}
}

@Unpublished{BehHofKup04,
  author = 	 {Gerd Behrmann and J{\"o}rg Hoffmann and Sebastian Kupferschmid},
  title = 	 {How to ``Ignore Delete Lists'' in Timed Automata},
  note = 	 {Draft presented at AVACS meeting September 2004,
                  later submitted as \cite{KupHofDieBeh05}},
  year =         {2004}
}

@InProceedings{B95,
  author = 	 {Christoph Beierle},
  title = 	 {Type Inferencing for Polymorphic Order-sorted Logic Programs},
  booktitle = 	 {Proceedings of the 12th International Conference
                  on Logic Programming},
  pages =	 {765--779},
  year =	 1995,
  editor =	 {Leon Sterling},
  publisher =	 {MIT Press}
}

@InProceedings{BelPod04,
  author = 	 {Nicolas Beldiceanu and Emmanuel Poder},
  title = 	 {The \textit{period} Constraint},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {329-342},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{BenYi04,
  author = 	 {Johan Bengtsson and
                  Wang Yi},
  title = 	 {Timed Automata: Semantics, Algorithms and Tools},
  booktitle = 	 {Lectures on Concurrency and Petri Nets 2003},
  pages =	 {87-124},
  year =	 2004,
  editor =	 {J{\"o}rg Desel and
               Wolfgang Reisig and
               Grzegorz Rozenberg},
  volume =	 3098,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag},
}

@InProceedings{BenSaiSie94,
  author = 	 {Belaid Benhamou and Lakhdar Sais and Pierre Siegel},
  title = 	 {Two proof procedures for a cardinality based language in propositional calculus},
  booktitle = 	 {Proceedings of the 11th Annual Symposium on Theoretical Aspects of Computer Science},
  year =	 1994,
  volume =	 775,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag},
  pages = {71-82}, 
  editor    = {Patrice Enjalbert and
               Ernst W. Mayr and
               Klaus W. Wagner},
}

@Book{BerBidFin01,
  author =	 {B{\'e}atrice Berard and Michel Bidoit and Alain Finkel 
                  and F. Laroussinie and
	          A. Petit and L. Petrucci and Ph. Schnoebelen},
  title = 	 {Systems and Software Verification: Model-Checking Techniques and Tools},
  publisher = 	 {Springer-Verlag},
 translator = {P. McKenzie},
  year = 	 2001
}
%blluebook

@InProceedings{BerFri99,
  author    = {B{\'e}atrice B{\'e}rard and Laurent Fribourg},  
  editor    = {Jos C. M. Baeten and
               Sjouke Mauw},
  title     = {Reachability Analysis of (Timed) {P}etri Nets Using Real Arithmetic},
  booktitle = {Proceedings of the 10th International Conference on Concurrency Theory},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {1664},
  year      = {1999},
  pages     = {178-193}
}

@InProceedings{BerNip00,
  author = 	 {S. Berghofer and T. Nipkow},
  title = 	 {Executing Higher Order Logic},
  booktitle = 	 {Proceedings of Types for Proofs and Programs},
  pages =	 {24-40},
  year =	 2000,
  editor =	 {P. Callaghan and Z. Luo and J. McKinna and R. Pollack},
  volume =	 2277,
  series =	 {LNCS},
  publisher =	 {Springer}
}

@Book{Bern99,
  author =	 {Tim {Berners-Lee}},
  title = 	 {Weaving the {W}eb},
  publisher = 	 {Harper},
  year = 	 1999
}

@Article{BerHenLas01,
  author = 	 {Tim {Berners-Lee} and James A. Hendler and Ora Lassila},
  title = 	 {The {S}emantic {W}eb},
  journal = 	 {Scientific American},
  year = 	 2001,
  volume =	 284,
  pages =	 {34-43}
}

@InProceedings{BerVarWol94,
  author    = {Orna Bernholtz and Moshe Y. Vardi and Pierre Wolper},
  editor    = {David L. Dill},
  title     = {An Automata-Theoretic
                  Approach to Branching-Time Model Checking},
  booktitle = {Proceedings of the 6th International Conference on 
               Computer Aided Verification},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {818},
  year      = {1994},
  pages     = {142-155},
  note      = {Extended Abstract. Bernholtz changed name to Kupfermann}
}

@InProceedings{BieCimClaZhu99,
  author = 	 {Armin Biere and Alessandro Cimatti and Edmund
                  M. Clarke and Yunshan Zhu},
  title = 	 {Symbolic Model Checking without {BDD}s},
  booktitle = 	 {5th International Conference on 
                  Tools and Algorithms for Construction and 
                  Analysis of Systems},
  pages =	 {193-207},
  year =	 1999,
  editor =	 {Rance Cleaveland},
  volume =	 1579,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{BieClaRaiZhu99,
  author = 	 {Armin Biere and Edmund M. Clarke and Richard Raimi and Yunshan Zhu},
  title = 	 {Verifiying
                  Safety Properties of a {Power} {PC} Microprocessor Using
                  Symbolic Model Checking without {BDD}s},
  booktitle = 	 {Proceedings of the 11th International Conference on 
                  Computer Aided Verification},
  pages =	 {60-71},
  year =	 1999,
  editor =	 {Nicolas Halbwachs and Doron Peled},
  volume =	 1633,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@inproceedings{BirMee98,
  author    = {Richard S. Bird and
               Lambert G. L. T. Meertens},
  editor    = {Johan Jeuring},
  title     = {Nested Datatypes},
  booktitle = {Proceedings of the Conference on 
               Mathematics of Program Construction},
  year      = {1998},
  pages     = {52-67},
  volume    = {1422},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{BluFur95,
  author = 	 {Avrim Blum and Merrick L. Furst},
  title = 	 {Fast Planning Through Planning Graph Analysis},
  booktitle = 	 {Proceedings of the 14th International Joint Conference on
                  Artificial Intelligence},
  pages =	 {1636-1642},
  year =	 1995,
  publisher =	 {Morgan Kaufmann},
  note =	 {2 volumes}
}

@Article{BluFur97,
  author = 	 {Avrim Blum and Merrick L. Furst},
  title = 	 {Fast Planning Through Planning Graph Analysis},
  journal = 	 {Artificial Intelligence},
  pages =	 {281-300},
  year =	 1997,
  volume = 	 {90},
  Tnumber = 	 {1-2}
}

@TechReport{BoeKraOls07,
  author = 	 {Thomas B{\o}gholm and Henrik Kragh-Hansen and Petur Olsen},
  title = 	 {Real-Time {J}ava},
  institution =  {Aalborg University},
  year = 	 2009,
  note =	 {Report on a study project}
}

@inproceedings{BogholmKOTL08,
  author    = {Thomas B{\o}gholm and
               Henrik Kragh-Hansen and
               Petur Olsen and
               Bent Thomsen and
               Kim Guldstrand Larsen},
  title     = {Model-based schedulability analysis of safety critical hard
               real-time {J}ava programs},
  booktitle = {JTRES},
  year      = {2008},
  pages     = {106-114},
  ee        = {http://doi.acm.org/10.1145/1434790.1434807},
  crossref  = {DBLP:conf/jtres/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/jtres/2008,
  editor    = {Gregory Bollella and
               C. Douglas Locke},
  title     = {Proceedings of the 6th International Workshop on {J}ava Technologies
               for Real-time and Embedded Systems, JTRES 2008, 24-26 September
               2008, Santa Clara, California, USA},
  booktitle = {JTRES},
  publisher = {ACM},
  series    = {ACM International Conference Proceeding Series},
  volume    = {343},
  year      = {2008},
  isbn      = {978-1-60558-337-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Unpublished{Bol11,
  author = 	 {Stefan Bolus},
  title = 	 {On Finding Weighted Representations of Simple Games
                  by Linear Programming and Binary Decision Diagrams},
  note = 	 {Received from the author},
  year =	 2011
}

@article{Bol11OR,
  author    = {Stefan Bolus},
  title     = {Power indices of simple games and vector-weighted majority
               games by means of binary decision diagrams},
  journal   = {European Journal of Operational Research},
  volume    = {210},
  number    = {2},
  year      = {2011},
  pages     = {258-272},
  ee        = {http://dx.doi.org/10.1016/j.ejor.2010.09.020},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@InProceedings{BonGef98,
  author = 	 {Blai Bonet and Hector Geffner},
  title = 	 {{HSP}: Heuristic Search Planner},
  booktitle = 	 {AIPS-98 Planning Competition},
  year =	 1998,
  address =	 {Pittsburgh, PA, USA}
}

@InBook{BocWei01,
  author =	 {A. Bockmayr and V. Weispfenning},
  title = 	 {Handbook of Automated Reasoning},
  chapter = 	 {Chapter 12: Solving Numerical Constraints},
  publisher = 	 {Elsevier},
  year = 	 2001
}

@Article{Bon04,
  author = 	 {Piero Bonatti},
  title = 	 {Reasoning with Infinite Stable Models},
  journal = 	 {Artificial Intelligence},
  year = 	 2004,
  volume =	 156,
  number =	 1,
  pages =	 {75-111}
}

@InProceedings{BonGef99,
  author = 	 {Blai Bonet and Hector Geffner},
  title = 	 {Planning as Heuristic Search: New
                  Results},
  booktitle = 	 {Proceedings of the 5th
                  European Conference on Planning},
  pages =	 {360-372},
  year =	 1999,
  editor =	 {Susanne Biundo and Maria Fox},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Article{BonGef01,
  author = 	 {Blai Bonet and Hector Geffner},
  title = 	 {Planning as Heuristic Search},
  journal = 	 {Artificial Intelligence},
  year = 	 2001,
  volume =	 129,
  number =	 {1-2},
  pages =	 {5-33}
}

@InProceedings{BonLoeGef97,
  author = 	 {Blai Bonet and G{\'a}bor Loerincs and Hector Geffner},
  title = 	 {A Robust and Fast Action
                  Selection Mechanism for Planning},
  booktitle = 	 {Proceedings of the 14th National Conference on Artificial
                  Intelligence and 9th Innovative Applications of
                  Artificial Intelligence Conference},
  pages =	 {714-719},
  year =	 1997,
  publisher =	 {AAAI Press / The MIT Press}
}

@Article{BorDovFog07,
  author = 	 {Luca Bortolussi and Agostino Dovier and Federico Fogolari},
  title = 	 {Agent-based Protein Structure Prediction},
  journal = 	 {Multiagent and Grid Systems},
  year = 	 2007,
  volume =	 3,
  number =	 2,
  pages =	 {183-197}
}

@article{BorPol08,
  author    = {Luca Bortolussi and
               Alberto Policriti},
  title     = {Modeling Biological Systems in Stochastic Concurrent Constraint
               Programming},
  journal   = {Constraints},
  volume    = {13},
  number    = {1-2},
  year      = {2008},
  pages     = {66-90}
}

@Proceedings{BosLeu02,
  title = 	 {Model Checking Software, 9th
International SPIN Workshop},
  year = 	 2002,
  editor =	 {Dragan Bosnacki and Stefan Leue},
  volume =	 2318,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{BC98,
  author = 	 {Annalisa Bossi and Nicoletta Cocco},
  title = 	 {Successes in Logic Programs},
  booktitle = 	 {Proceedings of the 8th International Workshop on 
                  Logic Program Synthesis and Transformation},
  year =	 1999,
  editor =	 {Pierre Flener},
  pages =        {219--239},
  publisher =	 {Springer-Verlag},
  series =	 {LNCS},
  volume =       {1559}
}

%Keine Konferenz. Special Volume
@InCollection{BosCocEtaRos04,
  author    = {Annalisa Bossi and
               Nicoletta Cocco and
               Sandro Etalle and
               Sabina Rossi},
  title     = {Declarative Semantics of Input Consuming Logic Programs},
  booktitle = 	 {Program Development in Computational Logic},
  publisher =	 {Springer-Verlag},
  year =	 2004,
  volume =       3049,
  editor =	 {Maurice Bruynooghe and Kung-Kiu Lau},
  series =	 {LNCS},
  pages     = {90-114}
}

@inproceedings{BosEtaRos00,
  author    = {Annalisa Bossi and
               Sandro Etalle and
               Sabina Rossi},
  title     = {Semantics of Input-Consuming Logic Programs},
  editor    = {John W. Lloyd and
               Ver{\'o}nica Dahl and
               Ulrich Furbach and
               Manfred Kerber and
               Kung-Kiu Lau and
               Catuscia Palamidessi and
               Lu\'{\i}s Moniz Pereira and
               Yehoshua Sagiv and
               Peter J. Stuckey},
  booktitle = {Proceedings of the 1st International Conference on Computational Logic},
  year      = {2000},
  pages     = {194-208},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {1861}
}

@article{BosEtaRos00-CL,
  author    = {Annalisa Bossi and
               Sandro Etalle and
               Sabina Rossi},
  title     = {Semantics of well-moded input-consuming logic programs},
  journal   = {Computer Languages},
  volume    = {26},
  number    = {1},
  year      = {2000},
  pages     = {1-25}
}

@article{Bou04,
  author    = {Patricia Bouyer},
  title     = {Forward Analysis of Updatable Timed Automata.},
  journal   = {Formal Methods in System Design},
  volume    = {24},
  number    = {3},
  year      = {2004},
  pages     = {281-320},
  publisher = {Springer-Verlag} 
}

@InProceedings{Bou03,
  author = 	 {Patricia Bouyer},
  title = 	 {Untameable Timed Automata!},
  booktitle = 	 {Proceedings of the 20th Annual Symposium on Theoretical Aspects of Computer
               Science},
  pages =	 {620-631},
  year =	 2003,
  editor =	 {Helmut Alt and
               Michel Habib},
  volume =	 2607,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag},
  note =	 {Extended Abstract}
}

@Misc{Bosnacki,
  author =	 {Dragan Bo{\v s}na{\v c}ki},
  title =	 {Digitization of Timed Automata},
  note =	 {Available from
                  \url{http://www.ii.edu.mk/algebraic\_structures/docs\%5Cdigit.ps}}
}

@article{BozBruCimJunRosSchSeb05,
  author    = {Marco Bozzano and
               Roberto Bruttomesso and
               Alessandro Cimatti and
               Tommi A. Junttila and
               Peter van Rossum and
               Stephan Schulz and
               Roberto Sebastiani},
  title     = {{MathSAT}: Tight Integration of {SAT} and Mathematical Decision
               Procedures},
  journal   = {Journal of Automated Reasoning},
  volume    = {35},
  number    = {1-3},
  year      = {2005},
  pages     = {265-293}
}

@InProceedings{BozCimColKirSeb04,
  author = 	 {M. Bozzano and A. Cimatti and G. Colombini and V. Kirov and
                  R. Sebastiani},
  title = 	 {The {MathSAT} solver -- a progress
                  report},
  booktitle = 	 {Proceedings of PDPAR},
  year =	 2004,
  address =	 {Cork, Ireland},
  note =	 {An extended version is available as
                  technical report.}
}

@InProceedings{BraDom06,
  author = 	 {Ronen I. Brafman and Carmel Domshlak},
  title = 	 {Factored Planning: How, When and When Not},
  booktitle = 	 {AAAI},
  year =	 2006
}

@inproceedings{BraCriDeVFit06,
  author    = {Martin Brain and
               Tom Crick and
               Marina De Vos and
               John Fitch},
  title     = {{TOAST}: Applying Answer Set Programming to Superoptimisation},
  editor    = {Sandro Etalle and
               Miros{\l}aw Truszczy{\'n}ski},
  booktitle     = {Proceedings of the 22nd International Conference on Logic Programming},
  year      = {2006},
  pages     = {270-284},
  publisher = {Springer-Verlag},
  series    = {LNCS}, 
  volume    = {4079}
}

@inproceedings{Bre07,
  author    = {Gerhard Brewka},
  title     = {Preferences, Contexts and Answer Sets},
  editor    = {Ver{\'o}nica Dahl and
               Ilkka Niemel{\"a}},
  publisher = {Springer-Verlag},
  volume    = {4670},
  series    = {LNCS},
  booktitle = {Proceedings pf the 23rd International Conference on Logic Programming},
  year      = {2007},
  pages     = {22}
}

@InProceedings{BCGV02,
  author =   {Maurice Bruynooghe and
               Michael Codish and
               Samir Genaim and
               Wim Vanhoof},
  title =    {Reuse of Results in Termination Analysis of
               Typed Logic Programs},
  booktitle =    {Proceedings of the 9th International Static Analysis Symposium},
  pages =    {477-492},
  year =     2002,
  editor =   {Manuel V. Hermenegildo and
               Germ{\'a}n Puebla},
  volume =   2477,
  publisher = {Springer-Verlag},
  series    = {LNCS}
}

@inproceedings{BruVanCod01,
  author    = {Maurice Bruynooghe and
               Wim Vanhoof and
               Michael Codish},
  title     = {{Pos(T)}: Analyzing Dependencies in Typed Logic Programs},
  editor    = {Dines Bj{\o}rner and
               Manfred Broy and
               Alexandre V. Zamulin},
  booktitle = {Proceedings of the 4th International Andrei
               Ershov Memorial Conference, Revised Papers},
  year      = {2001},
  pages     = {406-420},
  volume =   2244,
  publisher = {Springer-Verlag},
  series    = {LNCS}
}

@InProceedings{Bue62,
  author = 	 {Richard B{\"u}chi},
  title = 	 {On a Decision Method in Restricted Second-Order Arithmetic},
  booktitle = 	 {Proceedings of the International Congress on Logic,
                  Methodology, and Philosophy of Science 1960},
  pages =	 {1-12},
  year =	 1962,
  publisher =	 {Stanford University Press}
}

@Article{BurClaMcMDil92,
  author = 	 {J. R. Burch and E. M. Clarke and K. L. McMillan and D. L. Dill},
  title = 	 {Symbolic model checking: $10^{20}$ states
                  and beyond},
  journal = 	 {Information and Computation},
  year = 	 1992,
  volume =	 98,
  number =	 2,
  pages =	 {142-170},
  note =	 {Special Issue: Selections from 1990 IEEE Symposium
                  on Logic in Computer Science}
}

@InProceedings{Byl91,
  author = 	 {Tom Bylander},
  title = 	 {Complexity Results for Planning},
  booktitle = 	 {Proceedings of the 12th International Joint Conference on Artificial Intelligence},
  pages =	 {274-279},
  year =	 1991,
  editor =	 {John Mylopoulos and Raymond Reiter}
}

@InProceedings{CasRou01,
  author = 	 {Pierre Cast{\'e}ran and Davy Rouillard},
  title = 	 {Towards a Generic Tool for Reasoning about Labeled
                  Transition Systems},
  booktitle = 	 {TPHOLS Supplemental Proceedings},
  pages =	 {98-106},
  year =	 2001,
  editor =	 {Richard J. Boulton and Paul B. Jackson},
  series =	 {Informatics Research Report EDI-INF-RR-0046},
  address =	 {Edinburgh}
}

@inproceedings{ChaKue03,
  author =    {Donald Chai and Andreas Kuehlmann},
  title =     {A fast pseudo-{B}oolean constraint solver},
  booktitle = {Proceedings of the 40th Design Automation Conference},
  publisher = {ACM},
  year      = {2003},
  pages =     {830-835}
}

@inproceedings{ChaClaGroJhaVei03,
  author    = {Sagar Chaki and
               Edmund M. Clarke and
               Alex Groce and
               Somesh Jha and
               Helmut Veith},
  title     = {Modular Verification of Software Components in {C}},
  booktitle = {Proceedings of the 25th International Conference on Software
               Engineering},
  year      = {2003},
  pages     = {385-395},
  publisher = {IEEE Computer Society}
}

@article{ChaHanParZia04,
 author = {Jean-Marc Champarnaud and Georges Hansel and Thomas Parantho\"{e}n and Djelloul Ziadi},
 title = {Random generation models for NFA'S},
 journal = {J. Autom. Lang. Comb.},
 volume = {9},
 number = {2-3},
 year = {2004},
 issn = {1430-189X},
 pages = {203--216},
 publisher = {Otto-von-Guericke-Universitat},
 address = {Magdeburg, Germany, Germany},
 }


@InProceedings{Cha88,
  author = 	 {D. Chan},
  title = 	 {Constructive Negation Based on the Complete Database},
  booktitle = 	 {Proceedings of ICLP'88},
  pages =	 {111-125},
  year =	 1988,
  publisher =	 {MIT Press}
}

@InProceedings{Cha89,
  author = 	 {D. Chan},
  title = 	 {An Extension of Constructive Negation and its
                  Application to Coroutining},
  booktitle = 	 {Proceedings of NACLP'89},
  pages =	 {477-493},
  year =	 1989,
  publisher =	 {MIT Press}
}

@InProceedings{ChaPod98,
  author    = {Witold Charatonik and Andreas Podelski},
  editor    = {Bernhard Steffen},
  booktitle = {Proceedings of the 4th International Conference on
               Tools and Algorithms for Construction and Analysis of Systems},
  title     = {Set-Based Analysis of Reactive Infinite-State Systems},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {1384},
  year      = {1998},
  pages     = {358-375}
}

@InProceedings{CheUrb04,
  author = 	 {James Cheney and Christian Urban},
  title = 	 {$\alpha$Prolog: A Logic Programming Language with Names,
                  Binding and $\alpha$-Equivalence},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {269-283},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Article{ChoPel99,
  author = 	 {Ching-Tsun Chou and Doron Peled},
  title = 	 {Formal Verification of a Partial-Order Reduction Technique for
                  Model Checking},
  journal = 	 {Journal of Automated Reasoning},
  year = 	 1999,
  volume =	 23,
  number =	 {3-4},
  pages =	 {265-298}
}

@InProceedings{ChrDah04,
  author = 	 {Henning Christiansen and Veronica Dahl},
  title = 	 {Assumptions and Abduction in {P}rolog},
  booktitle = 	 {Proceedings of 14th Workshop on Logic Programming
                  Environments and 3rd Workshop on Multiparadigm
                  Constraint Programming},
  year =	 2004,
  pages =        {87-102},
  editor =	 {Susana Mu{\~n}oz-Hern{\'a}ndez and Jos{\'e} Manuel G{\'o}mez-Perez
                  and Petra Hofstedt},
  note =	 {Held in conjunction with ICLP04}
}

@Article{ChuKro03,
  author = 	 {C. Chutinan and B.H Krogh},
  title = 	 {Computational Techniques for Hybrid System Verification},
  journal = 	 {IEEE Transactions on Automatic Control},
  year = 	 2003,
  volume =	 48,
  number =	 1,
  pages =	 {64-75}
}

@inproceedings{ClaEme81,
  author    = {Edmund M. Clarke and
               E. Allen Emerson},
  title     = {Design and Synthesis of Synchronization Skeletons Using
               Branching-Time Temporal Logic},
  editor    = {Dexter Kozen},
  booktitle = {Proceedings of the Workshop on Logic of Programs},
  year      = {1982},
  pages     = {52-71},
  series    = {LNCS},
  publisher = {Springer-Verlag},
  volume    = {131}
}

@Book{ClaGruPel02,
  author =	 {Edmund M. Clarke and Orna Grumberg and Doron A. Peled},
  title = 	 {Model Checking},
  publisher = 	 {MIT Press},
  year = 	 2002,
  note =	 {5th print}
}

@Article{ClaGupStr04,
  author = 	 {Edmund Clarke and Anubhav Gupta and Ofer Strichman},
  title = 	 {{SAT}-based Counterexample-Guided Abstraction Refinement},
  journal = 	 {IEEE Transactions on Computer Aided Design},
  year = 	 2004,
  volume =	 23,
  number =	 7,
  pages =	 {1113-1123}
}

@inproceedings{ClaFehHanKroStuThe03,
  author    = {Edmund M. Clarke and
               Ansgar Fehnker and
               Zhi Han and
               Bruce H. Krogh and
               Olaf Stursberg and
               Michael Theobald},
  editor    = {Hubert Garavel and
               John Hatcliff},
  title     = {Verification of Hybrid Systems Based on Counterexample-Guided
               Abstraction Refinement},
  booktitle = {Proceedings of the 9th International Conference on 
               Tools and Algorithms for the Construction and Analysis of
               Systems},
  year      = {2003},
  pages     = {192-207},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {2619}
}

@TechReport{ClaFehHanKroOuaStuThe03,
  author = 	 {Edmund M. Clarke and
               Ansgar Fehnker and
               Zhi Han and
               Bruce H. Krogh and
               Jo{\"e}l Ouaknine and 
               Olaf Stursberg and
               Michael Theobald},
  title = 	 {Abstraction and Counterexample-Guided Refinement in
                  Model Checking of Hybrid Systems},
  institution =  {CMU},
  year = 	 2003,
  number =	 {CMU-CS-03-104}
}

@Article{CoaLew61,
  author = 	 {Clarence L. Coates and Philip M. {Lewis II}},
  title = 	 {Linearly-separable Switching Functions},
  journal = 	 {Journal of Franklin Institute},
  year = 	 1961,
  volume =	 272,
  pages =	 {366-410},
  note =	 {Also in an expanded version, GE Research Laboratory,
                  Schenectady, N.Y., Technical Report No.61-RL-2764E}
}

@Article{CoaKirLew62,
  author = 	 {Clarence L. Coates and R. B. Kirchner and Philip M. {Lewis II}},
  title = 	 {A Simplified Procedure for the Realization of
                  Linearly-Separable Switching Functions},
  journal = 	 {{IRE} Transactions on Electronic Computers},
  year = 	 1962
}

@InProceedings{CobClaOst01,
  author = 	 {Jamieson M. Cobleigh and Lori A. Clarke and Leon J. Osterweil},
  title = 	 {The Right Algorithm at the Right Time: Comparing
                  Data Flow Analysis Algorithms for Finite State Verification},
  booktitle = 	 {Proceedings of the 23rd International Conference on Software
               Engineering},
  pages =	 {37-46},
  year =	 2001,
  publisher =	 {IEEE Computer Society}
}

@InProceedings{CGBH94,
  author = 	 {Mike Codish and Maria {Garc\'{\i}a de la Banda} and
                  Maurice Bruynooghe and Manuel Hermenegildo},
  title = 	 {Goal Dependent versus Goal Independent Analysis of Logic Programs},
  booktitle = 	 {Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning},
  pages =	 {305--319},
  year =	 1994,
  volume =       {822},
  editor =	 {Frank Pfenning},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{ConDan93,
  author = 	 {C. Consel and O. Danvy},
  title = 	 {Tutorial Notes on Partial Evaluation},
  booktitle = 	 {Proceedings of the 20th Annual ACM Symposium on
                  Principles of Programming Languages},
  pages =	 {493-501},
  year =	 1993,
  publisher =	 {ACM Press}
}

@Article{CooCouTur87,
  author = 	 {W. Cook and C.R. Coullard and G. Turan},
  title = 	 {On the complexity of cutting-plane proofs},
  journal = 	 {Discrete Applied Mathematics},
  year = 	 1987,
  volume =	 18,
  pages =	 {25-38},
  note = {Not in DBLP database}  
}

@article{CouVarWolYan92,
  author    = {Costas Courcoubetis and
               Moshe Y. Vardi and
               Pierre Wolper and
               Mihalis Yannakakis},
  title     = {Memory-Efficient Algorithms for the Verification of Temporal
               Properties},
  journal   = {Formal Methods in System Design},
  volume    = {1},
  number    = {2/3},
  year      = {1992},
  pages     = {275-288},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Inproceedings{CouCou77,
Author       ="Patrick Cousot and Radhia Cousot",
Title        ={Abstract Interpretation: a Unified Lattice
Model for Static Analysis of Programs by Construction or
Approximation of Fixpoints},  
Year         ={1977},
Booktitle    ={Proceedings of the 4th {ACM} Symposium on Principles of
               Programming Languages}, 
Pages        ={238--252}
}

@inproceedings{Cou99,
  author    = {Jean-Michel Couvreur},
  title     = {On-the-Fly Verification of Linear Temporal Logic},
  booktitle = {World Congress on Formal Methods},
  year      = {1999},
  pages     = {253-271},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/1708/17080253.htm},
  crossref  = {fm1999},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{fm1999,
  editor    = {Jeannette M. Wing and
               Jim Woodcock and
               Jim Davies},
  title     = {FM'99 - Formal Methods, World Congress on Formal Methods
               in the Development of Computing Systems, Toulouse, France,
               September 20-24, 1999, Proceedings, Volume I},
  booktitle = {World Congress on Formal Methods},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1708},
  year      = {1999},
  isbn      = {3-540-66587-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{Cra57,
  author = 	 {William Craig},
  title = 	 {Three Uses of the {H}erbrand-{G}entzen Theorem in
                  Relating Model Theory and Proof Theory},
  journal = 	 {Journal of Symbolic Logic},
  year = 	 1957,
  volume =	 22,
  number =	 3,
  pages =	 {269-285}
}

@Book{CraHam07,
 author = 		{Yves Crama and Peter L. Hammer},
 title	=		{{Boolean Functions: Theory, Algorithms, and Applications}},
 publisher = 	{Cambridge University Press},
 year	=		{2011},
 series	=		{Encyclopedia of Mathematics and its Applications},
 month	=		{May},
 isbn	=		{0521847516}
}

@Book{CraHam11,
 author = 		{Yves Crama and Peter L. Hammer},
 title	=		{{Boolean Functions: Theory, Algorithms, and Applications}},
 publisher = 	{Cambridge University Press},
 year	=		{2011},
 series	=		{Encyclopedia of Mathematics and its Applications},
 month	=		{May},
 isbn	=		{0521847516}
}

@Article{CruBar04,
  author = 	 {Jorge Cruz and Pedro Barahona},
  title = 	 {Constraint Reasoning with Differential Equations},
  journal = 	 {Applied Numerical Analysis \& Computational
                  Mathematics}, 
  year = 	 2004,
  volume =	 1,
  number =	 1,
  pages =	 {140-154}
}

@InProceedings{CulSch96,
  author = 	 {Joseph C. Culberson and Jonathan Schaeffer},
  title = 	 {Searching with Pattern Databases},
  booktitle = 	 {Proceedings  of the 11th Biennial Conference of the
                  Canadian Society for Computational Studies of
                  Intelligence},
  pages =	 {402-416},
  year =	 1996,
  editor =	 {Gordon I. McCalla},
  volume =	 1081,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Article{CulSch98,
  author = 	 {Joseph C. Culberson and Jonathan Schaeffer},
  title = 	 {Pattern Databases},
  journal = 	 {Computational Intelligence},
  year = 	 1998,
  volume =	 14,
  number =	 3,
  pages =	 {318-334}
}

@InProceedings{CumFabGreLeo04,
  author = 	 {Chiara Cumbo and Wolfgang Faber and Gianluigi greco
                  and Nicola Leone},
  title = 	 {Enhancing the Magic-Set Method for Disjunctive Datalog
  Programs},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {371-385},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@article{DalDovWil08,
  author    = {Alessandro {Dal Pal{\`u}} and
               Agostino Dovier and
               Sebastian Will},
  title     = {Introduction to the Special Issue on Bioinformatics and
               Constraints},
  journal   = {Constraints},
  volume    = {13},
  number    = {1-2},
  year      = {2008},
  pages     = {1-2}
}

@InProceedings{DanSol10,
  author = 	 {Evgeny Dantsin and Sergei Soloviev},
  title = 	 {Algorithms in Games Evolving in Time: Winning Strategies
                  Based on Testing Hypotheses},
  booktitle = 	 {Proceedings of the 2nd Workshop on Games for Design,
                  Verification and Synthesis},
  year =	 2010,
  editor =	 {Kim G. Larsen and
    Nicolas Markey and
    Jean-Fran{\c c}ois Raskin and
    Wolfgang Thomas},
  note =	 {CONCUR'10 workshop}
}

@article{DarMar02,
  author    = {Adnan Darwiche and
               Pierre Marquis},
  title     = {A Knowledge Compilation Map},
  journal   = {Journal of Artificial Intelligence Research},
  volume    = {17},
  year      = {2002},
  pages     = {229-264}
}

@inproceedings{DasDil02,
  author    = {Satyaki Das and
               David L. Dill},
  title     = {Counter-Example Based Predicate Discovery in Predicate Abstraction},
  editor    = {Mark Aagaard and
               John W. O'Leary},
  booktitle = {Proceedings of the 4th International
               Conference on Formal Methods in Computer-Aided Design},
  year      = {2002},
  pages     = {19-32},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {2517}
}

@inproceedings{DavidLLNW10,
  author    = {Alexandre David and
               Kim G. Larsen and
               Axel Legay and
               Ulrik Nyman and
               Andrzej Wasowski},
  title     = {Timed {I/O} automata: a complete specification theory for
               real-time systems},
  booktitle = {HSCC},
  year      = {2010},
  pages     = {91-100},
  ee        = {http://doi.acm.org/10.1145/1755952.1755967},
  crossref  = {DBLP:conf/hybrid/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/hybrid/2010,
  editor    = {Karl Henrik Johansson and
               Wang Yi},
  title     = {Proceedings of the 13th ACM International Conference on
               Hybrid Systems: Computation and Control, HSCC 2010, Stockholm,
               Sweden, April 12-15, 2010},
  booktitle = {HSCC},
  publisher = {ACM ACM},
  year      = {2010},
  isbn      = {978-1-60558-955-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{DavLogLov62,
  author = 	 {Martin Davis and George Logemann and Donald W. Loveland},
  title = 	 {A machine program
                  for theorem-proving},
  journal = 	 {Communications of the ACM},
  year = 	 1962,
  volume =	 5,
  number =	 7,
  pages =	 {394-397}
}

@Article{DavPut60,
  author = 	 {M. Davis and H. Putnam},
  title = 	 {A Computing Procedure for Quantification Theory},
  journal = 	 {Journal of the ACM},
  year = 	 1960,
  volume =	 7,
  pages =	 {201-215}
}

@inproceedings{DawTri98,
  author    = {Conrado Daws and
               Stavros Tripakis},
  title     = {Model Checking of Real-Time Reachability Properties Using
               Abstractions},
  booktitle = {TACAS},
  year      = {1998},
  pages     = {313-329},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/1384/13840313.htm},
  crossref  = {DBLP:conf/tacas/1998},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/tacas/1998,
  editor    = {Bernhard Steffen},
  title     = {Tools and Algorithms for Construction and Analysis of Systems,
               4th International Conference, TACAS '98, Held as Part of
               the European Joint Conferences on the Theory and Practice
               of Software, ETAPS'98, Lisbon, Portugal, March 28 - April
               4, 1998, Proceedings},
  booktitle = {TACAS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1384},
  year      = {1998},
  isbn      = {3-540-64356-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{DDLMS98,
  author =   {Stefaan Decorte and
               Danny {De Schreye} and
               Michael Leuschel and
               Bern Martens and
               Konstantinos F. Sagonas},
  title =    {Termination Analysis for Tabled Logic Programming},
  booktitle = {Proceedings of the 7th International Workshop on
               Logic Programming Synthesis and Transformation},
  editor    = {Norbert E. Fuchs},
series = {LNCS},
volume = 1463,
  publisher = {Springer-Verlag},
year = 1998,
pages = {111--127}
}

@InProceedings{DelPod99,
  author = 	 {Giorgio Delzanno and Andreas Podelski},
  title = 	 {Model Checking in {CLP}},
  booktitle = 	 {Proceedings of the 5th International Conference
                  on Tools and Algorithms for Construction and 
                  Analysis of Systems},
  pages =	 {223-239},
  year =	 1999,
  editor =	 {Rance Cleaveland},
  volume =	 1579,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Article{DelPod01,
  author = 	 {Giorgio Delzanno and Andreas Podelski},
  title = 	 {Constraint-based deductive model checking},
  journal = 	 {International Journal on Software Tools for Technlogy},
  year = 	 2001,
  publisher =	 {Springer-Verlag},
  volume =	 3,
  pages =	 {250-270}
}

@inproceedings{DeWDoyMaqRas08,
  author    = {Martin {De Wulf} and
               Laurent Doyen and
               Nicolas Maquet and
               Jean-Fran\c{c}ois Raskin},
  title     = {Antichains: Alternative Algorithms for {LTL} Satisfiability
               and Model-Checking},
  booktitle = {Proceedings of the 14th International Conference on 
               Tools and Algorithms for the Construction and Analysis of
               Systems},
  year      = {2008},
  pages     = {63-77},
  crossref  = {tacas08},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{tacas08,
  editor    = {C. R. Ramakrishnan and
               Jakob Rehof},
  title     = {Proceedings of the 14th International Conference on 
               Tools and Algorithms for the Construction and Analysis of
               Systems},
  booktitle = {TACAS},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {4963},
  year      = {2008}
}

@InProceedings{DeMDovMonPia06,
  author = 	 {Elisabetta {De Maria} and Agostino Dovier and Angelo Montanari 
                  and Carla Piazza},
  title = 	 {Exploiting Model Checking in Constraint-Based Approaches 
                  to the Protein Folding},
  booktitle =	 {Proceedings of the Workshop on Constraint Based Methods for Bioinformatics},
  pages =	 {46-54},
  year =	 2006
}

@InCollection{Dem08,
  author = 	 {Bart Demoen},
  title = 	 {My Life as a {P}rolog Implementor},
  booktitle = 	 {Newsletter},
  publisher =	 {Association for Logic Programming},
  year =	 2008,
  month =	 {February},
  note =	 {Available from \url{http://www.logicprogramming.org/newsletter/}}
}

@inproceedings{DGHMS99,
  author    = {Bart Demoen and
               Maria {Garc\'{\i}a de la Banda} and
               Warwick Harvey and
               Kim Marriott and
               Peter J. Stuckey},
  editor    = {Joxan Jaffar},
  title     = {An Overview of {HAL}},
  booktitle = {Proceedings of the 5th International Conference on 
               Principles and Practice of Constraint Programming},
  year      = {1999},
  pages     = {174-188},
  volume    = {1713},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Book{DerEdDCer96,
  author =	 {Deransart, Pierre and {Ed-Dbali}, Abdel Ali and Cervoni, Laurent},
  title = 	 {{P}rolog: The Standard},
  publisher = 	 {Springer-Verlag},
  year = 	 1996
}

@InProceedings{Der04,
  author = 	 {Nachum Dershowitz},
  title = 	 {Termination by Abstraction},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {1-18},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{Die97,
  author    = {Henning Dierks},
  title      = {{PLC}-automata: a new class of implementable real-time
                  automata},
  editor    = {Miquel Bertran and
               Teodor Rus},
  booktitle = {Proceedings of the 4th International
               AMAST Workshop on Real-Time Systems and Concurrent and Distributed
               Software},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {1231},
  year      = {1997},
  pages     = {61-93},
  note      = {Also appeared in TCS 253(1), 2001}
}

@Article{Die04,
  author =	 {Henning Dierks},
  title =	 {Comparing Model Checking and Logical Reasoning for
                  Real-Time Systems},
  journal =	 {Formal Aspects of Computing},
  year =	 2004,
  volume =	 16,
  number =	 2,
  pages =	 {104--120},
}

@InProceedings{Die05,
  author = 	 {Henning Dierks},
  title = 	 {Finding Optimal Plans for Domains with Restricted
  Continuous Effects with \textsc{Cora}}, 
  booktitle = 	 {Proceedings of the International Conference on
                  Automated Planning and Scheduling},
  year =	 2005,
  editor =	 {Susanne Biundo and Karen Myers and Kanna Rajan},
  note = {Did not actually find that on the ICAPS webpage} 
}

@inproceedings{DieFehMadVaa98,
  author    = {Henning Dierks and
               Ansgar Fehnker and
               Angelika Mader and
               Frits W. Vaandrager},
  title     = {Operational and Logical Semantics for Polling Real-Time
               Systems},
  editor    = {Anders P. Ravn and
               Hans Rischel},
  booktitle = {Proceedings of the 5th International Symposium on 
               Formal Techniques in Real-Time and Fault-Tolerant Systems},
  year      = {1998},
  pages     = {29-40},
  series    = {LNCS},
  publisher = {Springer-Verlag},
  volume    = {1486}
}

@InProceedings{DieKup07,
  author = {Henning Dierks and Sebastian Kupferschmid and Kim G.
                  Larsen},
  title = 	 {Automatic Abstraction Refinement for Timed Automata},
  editor    = {Jean-Fran\c{c}ois Raskin and
               P. S. Thiagarajan},
  year = 	 2007,
  pages     = {114-129},
  booktitle =	 {Proceedings of the 5th International Conference on
                  Formal Modelling and Analysis of Timed Systems},
  publisher = {Springer-Verlag},
  volume    = {4763},
  series = {LNCS}
}

@inproceedings{DH88,
  author    = {Roland Dietrich and
               Frank Hagl},
  title     = {A Polymorphic Type System with Subtypes for {P}rolog},
  editor    = {Harald Ganzinger},
  booktitle = {Proceedings of the 2nd European Symposium on Programming},
  pages     = {79-93},
  volume    = {300},
  year      = {1988},  
  series    = {LNCS},
  publisher = {Springer-Verlag}
}

@InProceedings{DilWon95,
  author = 	 {David L. Dill and Howard Wong-Toi},
  title = 	 {Verification of Real-Time Systems by
                  Successive Over and Under Approximation},
  booktitle = 	 {Proceedings of the 7th  International Conference on
                  Computer Aided Verification},
  pages =	 {409-422},
  year =	 1995,
  editor =	 {Pierre Wolper},
  volume =	 939,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@PhdThesis{Dix04,
  author = 	 {Heidi E. Dixon},
  title = 	 {Automating Pseudo-{B}oolean Inference within a
                  {DPLL} Framework},
  school = 	 {University of Oregon},
  year = 	 2004
}

@Article{DixGin00,
  author = 	 {Heidi E. Dixon and Matthew L. Ginsberg},
  title = 	 {Combining satisfiability techniques
                  from {AI} and {OR}},
  journal = 	 {The Knowledge Engineering Review},
  year = 	 2000,
  volume =	 15,
  pages =	 {31-45},
  note =	 {My version has 22 pages and dates from
                  2002. Bibliographical details of that version unknown}
}

@Article{DixGin-KER00,
  author = 	 {Heidi E. Dixon and Matthew L. Ginsberg},
  title = 	 {Combining satisfiability techniques
                  from {AI} and {OR}},
  journal = 	 {The Knowledge Engineering Review},
  year = 	 2000,
  volume =	 15,
  pages =	 {31-45}
}

@inproceedings{DonMal07,
  author    = {Alexandre Donz{\'e} and
               Oded Maler},
  title     = {Systematic Simulation Using Sensitivity Analysis},
  booktitle = {HSCC},
  year      = {2007},
  pages     = {174-189},
  ee        = {http://dx.doi.org/10.1007/978-3-540-71493-4_16},
  crossref  = {DBLP:conf/hybrid/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/hybrid/2007,
  editor    = {Alberto Bemporad and
               Antonio Bicchi and
               Giorgio C. Buttazzo},
  title     = {Hybrid Systems: Computation and Control, 10th International
               Workshop, HSCC 2007, Pisa, Italy, April 3-5, 2007, Proceedings},
  booktitle = {HSCC},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4416},
  year      = {2007},
  isbn      = {978-3-540-71492-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DovForPon07,
  author    = {Agostino Dovier and Andrea Formisano and Enrico Pontelli},
  title     = {Multivalued Action Languages with Constraints in {CLP(FD)}},
  editor    = {Ver{\'o}nica Dahl and
               Ilkka Niemel{\"a}},
  publisher = {Springer-Verlag},
  volume    = {4670},
  series    = {LNCS},
  booktitle = {Proceedings of the 23rd International Conference on Logic Programming},
  year      = {2007},
  pages     = {255-270}
}

@inproceedings{DoyRas07,
  author    = {Laurent Doyen and
               Jean-Fran\c{c}ois Raskin},
  title     = {Improved Algorithms for the Automata-Based Approach to Model-Checking},
  booktitle = {Proceedings of the 13th International Conference on 
               Tools and Algorithms for the Construction and Analysis of
               Systems},
  year      = {2007},
  pages     = {451-465},
  crossref  = {tacas07}
}

@proceedings{tacas07,
  editor    = {Orna Grumberg and
               Michael Huth},
  title     = {Proceedings of the 13th International Conference on 
               Tools and Algorithms for the Construction and Analysis of
               Systems},
  booktitle = {TACAS},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {4424},
  year      = {2007}
}


@Unpublished{DraFin05,
  author = 	 {Klaus Dr{\"a}ger and Bernd Finkbeiner},
  title = 	 {Abstracting Synchronisation},
  note = 	 {Presentation at AVACS Meeting R3, Oldenburg},
  year =	 2005
}

@Unpublished{DraFinPod05,
  author = 	 {Klaus Dr{\"a}ger and Bernd Finkbeiner and Andreas Podelski},
  title = 	 {Relaxation-based Model Checking},
  note = 	 {Submitted},
  year =	 2005
}

@inproceedings{DraFinPod06,
  author    = {Klaus Dr{\"a}ger and
               Bernd Finkbeiner and
               Andreas Podelski},
  title     = {Directed Model Checking with Distance-Preserving Abstractions},
  booktitle = {Proceedings of the 13th International SPIN Workshop on Model Checking Software},
  year      = {2006},
  pages     = {19-34},
  editor    = {Antti Valmari},
  series    = {LNCS},
  publisher = {Springer-Verlag},
  volume    = {3925}
}

@Book{DreBec98,
  author =	 {Rolf Drechsler and Bernd Becker},
  title = 	 {Binary Decision Diagrams - Theory and Implementation},
  publisher = 	 {Kluwer Academic Publishers},
  year = 	 1998
}

@InProceedings{DHM95,
  author = 	 {D. Dussart and F. Henglein and C. Mossin},
  title = 	 {Polymorphic Recursion and Subtype Qualifications:
  Polymorphic Binding-Time Analysis in Polynomial Time},
  booktitle = 	 {Proceedings of the Static Analysis Symposium},
  pages =	 {118-136},
  year =	 1995,
  editor =	 {A. Mycroft},
  volume =	 983,
  series =       {LNCS},
  publisher =	 {Springer-Verlag}
}

@article{DwoGreNilSchSel08,
  author    = {Steve Dworschak and
               Susanne Grell and
               Victoria J. Nikiforova and
               Torsten Schaub and
               Joachim Selbig},
  title     = {Modeling Biological Networks by Action Languages via Answer
               Set Programming},
  journal   = {Constraints},
  volume    = {13},
  number    = {1-2},
  year      = {2008},
  pages     = {21-65}
}

@inproceedings{DutMou06,
  author    = {Dutertre, Bruno  and
               Leonardo {Mendon\c{c}a de Moura}},
  title     = {A Fast Linear-Arithmetic Solver for {DPLL(T)}},
  editor    = {Thomas Ball and
               Robert B. Jones},
  booktitle = {Proceedings of the 18th International Conference on Computer Aided Verification},
  year      = {2006},
  pages     = {81-94},
  publisher = {Springer-Verlag},
  series    = {LNCS}
}

@InProceedings{Ede01,
  author = 	 {Stefan Edelkamp},
  title = 	 {Planning with Pattern Databases},
  booktitle = 	 {Proceedings of the European Conference on Planning},
  year =	 2001,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Inproceedings{Ede02,
  author    = {Stefan Edelkamp},
  title     = {Symbolic Pattern Databases in Heuristic Search Planning},
  editor    = {Malik Ghallab and
               Joachim Hertzberg and
               Paolo Traverso},
  booktitle = {Proceedings of the 6th International Conference on Artificial
               Intelligence Planning Systems},
  publisher = {AAAI},
  year      = {2002},
  pages     = {274-283}
}

@InProceedings{Ede03,
author = {Stefan Edelkamp},
title = {{Limits and Possibilities of {PDDL} for Model Checking Software}},
booktitle = {Proceedings of {ICAPS}'03 Workshop on the Competition: 
Impact, Organization, Evaluation, Benchmarks},
year = {2003},
month = {June},
address = {\url{http://icaps03.itc.it/satellite\_events/documents/WS/WS1/09/limits.pdf}}
}

@InProceedings{Ede05,
  author = 	 {Stefan Edelkamp},
  title = 	 {External Symbolic Heuristic Search with Pattern Databases},
  booktitle = 	 {Proceedings of the International Conference on
                  Automated Planning and Scheduling},
  year =	 2005,
  editor =	 {Susanne Biundo and Karen Myers and Kanna Rajan}
}

@inproceedings{EdeJab06,
  author    = {Stefan Edelkamp and
               Shahid Jabbar},
  title     = {Large-Scale Directed Model Checking {LTL}},
  booktitle = {Proceedings of the 13th International SPIN Workshop},
  year      = {2006},
  pages     = {1-18},
  editor    = {Antti Valmari},
  publisher = {Springer-Verlag},
  series    = {LNCS}, 
  volume    = {3925},
  year      = {2006}
}

@inproceedings{EdelkampLL01,
  author    = {Stefan Edelkamp and
               Alberto Lluch-Lafuente and
               Stefan Leue},
  editor    = {Matthew B. Dwyer},
  title     = {Directed Explicit Model Checking with {HSF-SPIN}},
  booktitle = {Proceedings of the 8th International {SPIN} Workshop},
  year      = {2001},
  pages     = {57-79},
  publisher = {Springer-Verlag},
  series    = {LNCS},
}

@Article{EdeLeuLlu04,
  author = 	 {Stefan Edelkamp and Stefan Leue and Alberto {Lluch-Lafuente}},
  title = 	 {Directed Explicit-State Model Checking in the Validation of Communication Protocols},
  journal = 	 {International Journal on Software Tools for Technology},
  year = 	 {2004},
  volume =	 {5},
  number =	 {2-3},
  pages =	 {247-267}
}


@Article{EdeLeuLlu04-POred,
  author = 	 {Stefan Edelkamp and Stefan Leue and Alberto {Lluch-Lafuente}},
  title = 	 {Partial Order Reduction and Trail Improvement in Directed Model Checking},
  journal = 	 {International Journal on Software Tools for Technology},
  year = 	 {2004},
  volume =	 {6},
  number =	 {4},
  pages =	 {277-301}
}

@TechReport{EdeLlu04,
  author = 	 {Stefan Edelkamp and Alberto Lluch-Lafuente},
  title = 	 {Abstraction Databases},
  institution =  {Computer Science Department, University of Freiburg},
  year = 	 2004,
  number =	 196
}

@InProceedings{EdeLlu04-icaps,
  author = 	 {Stefan Edelkamp and Alberto Lluch-Lafuente},
  title = 	 {Abstraction in Directed Model Checking},
  booktitle = 	 {Proceedings of the ICAPS Workshop on Connecting Planning Theory with Practice},
  pages =	 {7-13},
  year =	 {2004}
}

@inproceedings{EdeSch00,
  author    = {Stefan Edelkamp and
               Stefan Schr{\"o}dl},
  title     = {Localizing $\mathrm{A}^*$.},
  booktitle = {Proceedings of the 17th National Conference on Artificial
               Intelligence and 12th Conference on on Innovative Applications
               of Artificial Intelligence},
  year      = {2000},
  pages     = {885-890},
  publisher = {AAAI Press / The MIT Press},
}

@Article{EenSoe06,
  author = 	 {Niklas E{\'e}n and Niklas S{\"o}rensson},
  title = 	 {Translating Pseudo-{B}oolean Constraints into {SAT}},
  journal = 	 {Journal on Satisfiability, Boolean Modeling and Computation},
  year = 	 2006,
  volume =	 2,
  pages =	 {1-26}
}

@MastersThesis{Egg07,
  author = 	 {Andreas Eggers},
  title = 	 {Einbettung sicherer numerischer {I}ntegration von
                  {D}ifferentialgleichungen in {DPLL}-basiertes
                  arithmetisches {C}onstraint-{S}olving f{\"u}r hybride {S}ysteme},
  school = 	 {Universit{\"a}t Oldenburg},
  year = 	 2007
}

@InProceedings{EglSeiWol06,
  author = 	 {Uwe Egly and Martina Seidl and Stefan Woltran}, 
  title = 	 {A Solver for {QBF}s in  Nonprenex Form},
  booktitle = 	 {Proceedings of the 17th European Conference on
                  Artificial Intelligence},
  pages =	 {477-481},
  year =	 2006,
  editor =	 {Gerhard Brewka and Silvia Coradeschi and Anna Perini
                  and Paolo Traverso},
  publisher =	 {IOS Press}
}

@InProceedings{Ehlers/10/MinimisingDBA,
  author        = {R{\"u}diger Ehlers},
  title         = {Minimising Deterministic B{\"u}chi Automata Precisely Using SAT Solving},
  editor    = {O. Strichman and S. Szeider},
  booktitle     = "13th Thirteenth International Conference on Theory and Applications of Satisfiability
Testing (SAT 2010)",
  series = {LNCS},
  volume = {6175},
  year          = 2010,
  pages         = "326-332",
  publisher     = "Springer Verlag"
}

@inproceedings{EisKla06,
  author    = {Jochen Eisinger and
               Felix Klaedtke},
  title     = {Don't Care Words with an Application to the Automata-Based
               Approach for Real Addition},
  booktitle = {Proceedings of the  18th International Conference on 
               Computer Aided Verification},
  editor    = {Thomas Ball and
               Robert B. Jones},
  year      = {2006},
  pages     = {67-80},
  publisher = {Springer-Verlag},
  series    = {LNCS} 
}

@article{EitIbaMak02,
  author    = {Thomas Eiter and
               Toshihide Ibaraki and
               Kazuhisa Makino},
  title     = {Decision lists and related {B}oolean functions.},
  journal   = {Theor. Comput. Sci.},
  volume    = {270},
  number    = {1-2},
  year      = {2002},
  pages     = {493-524},
  ee        = {http://dx.doi.org/10.1016/S0304-3975(01)00003-2},
  bibsource = {DBLP, \url{http://dblp.uni-trier.de}}
}

@inproceedings{Eit07,
  author    = {Thomas Eiter},
  title     = {Answer Set Programming for the {S}emantic {W}eb},
  editor    = {Ver{\'o}nica Dahl and
               Ilkka Niemel{\"a}},
  publisher = {Springer-Verlag},
  volume    = {4670},
  series    = {LNCS},
  booktitle = {Proceedings of the 23rd International Conference on Logic Programming},
  year      = {2007},
  pages     = {23-26}
}

@inproceedings{ElkChaJen08,
  author    = {Edith Elkind and
               Georgios Chalkiadakis and
               Nicholas R. Jennings},
  title     = {Coalition Structures in Weighted Voting Games},
  booktitle = {ECAI},
  year      = {2008},
  pages     = {393-397},
  ee        = {http://dx.doi.org/10.3233/978-1-58603-891-5-393},
  crossref  = {DBLP:conf/ecai/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{ErdWon04,
  author = 	 {Esra Erdem and Martin D.F.~Wong},
  title = 	 {Rectilinear Steiner Tree Construction Uisng Answer Set
  Programming},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{EspKimKum04,
  author = 	 {J.M. Esposito and J. Kim and V. Kumar},
  title = 	 {Adaptive {RRT}s for Validating Hybrid Robotic
                  Control Systems},
  booktitle = 	 {WAFR},
  pages =	 {107-132},
  year =	 2004,
  address =	 {Zeist, Netherlands}
}


@inproceedings{EteHol00,
  author    = {Kousha Etessami and
               Gerard J. Holzmann},
  title     = {Optimizing {B}{\"u}chi Automata},
  booktitle = {CONCUR},
  year      = {2000},
  pages     = {153-167},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/1877/18770153.htm},
  crossref  = {concur2000},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{concur2000,
  editor    = {Catuscia Palamidessi},
  title     = {CONCUR 2000 - Concurrency Theory, 11th International Conference,
               University Park, PA, USA, August 22-25, 2000, Proceedings},
  booktitle = {CONCUR},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1877},
  year      = {2000},
  isbn      = {3-540-67897-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{FagSol08,
  author    = {Fran\c{c}ois Fages and
               Sylvain Soliman},
  title     = {Abstract Interpretation and Types for Systems Biology},
  journal   = {Theoretical Computer Science},
  volume    = {403},
  number    = {1},
  year      = {2008},
  pages     = {52-70}
}

@inproceedings{FagSol08-PILP,
  author    = {Fran\c{c}ois Fages and
               Sylvain Soliman},
  title     = {Model Revision from Temporal Logic Properties in Computational
               Systems Biology},
  year      = {2008},
  pages     = {287-304},
  booktitle     = {Probabilistic Inductive Logic Programming - Theory and Applications},
  volume    = {4911},
  editor    = {Luc {De Raedt} and
               Paolo Frasconi and
               Kristian Kersting and
               Stephen Muggleton},
  series    = {LNCS},
  publisher = {Springer-Verlag}
}

@inproceedings{FelMesHolKor04,
  author    = {Ariel Felner and
               Ram Meshulam and
               Robert C. Holte and
               Richard E. Korf},
  title     = {Compressing Pattern Databases},
  booktitle = {Proceedings of the 19th National Conference on Artificial
               Intelligence and the 16th Conference on Innovative Applications
               of Artificial Intelligence},
  editor    = {Deborah L. McGuinness and
               George Ferguson},
  year      = {2004},
  pages     = {638-643},
  publisher = {AAAI Press / The MIT Press}
}

@article{FelKorHan04,
  author    = {Ariel Felner and
               Richard E. Korf and
               Sarit Hanan},
  title     = {Additive Pattern Database Heuristics},
  journal   = {Journal of Artifical Intelligence Research},
  volume    = {22},
  year      = {2004},
  pages     = {279-318}
}

@Book{FenWahLieHen02,
  editor =	 {Dieter Fensel and Wolfgang Wahlster and Henry
                  Lieberman and James A. Hendler},
  title = 	 {Spinning the {S}emantic {W}eb: Bringing the {W}orld
                  {W}ide {W}eb to its Full Potential},
  publisher = 	 {MIT Press},
  year = 	 2002
}

@InProceedings{FiaMosShaShiTar89,
  author = 	 {Amos Fiat and Shahar Moses and Adi Shamir and Ilan
                  Shimshoni and G{\'a}bor Tardos},
  title = 	 {Planning and Learning in Permutation Groups},
  booktitle = 	 {proceedings of the 30th Annual Symposium on Foundations of Computer Science},
  pages =	 {274-279},
  year =	 1989,
  organization = {ACM}
}

@InProceedings{FilOwrRueSha01,
  author = 	 {Jean-Christophe Filli{\^a}tre and Sam Owre and Harald
                  Rue{\ss} and Natarajan Shankar},
  title = 	 {{ICS}: Integrated Canonizer and Solver},
  booktitle = 	 {Proceedings of the 13th International Conference on
                  Computer Aided Verification},
  pages =	 {246-249},
  year =	 2001,
  editor =	 {G{\'e}rard Berry and Hubert Comon and
                  Alain Finkel},
  volume =	 2102,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@article{FinkbeinerPS10,
  author    = {Bernd Finkbeiner and
               Hans-J{\"o}rg Peter and
               Sven Schewe},
  title     = {Synthesising certificates in networks of timed automata},
  journal   = {IET Software},
  volume    = {4},
  number    = {3},
  year      = {2010},
  pages     = {222-235},
  ee        = {http://dx.doi.org/10.1049/iet-sen.2009.0047},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{FKS95,
  author = 	 {B. Fischer and M. Kievernagel and W. Struckmann},
  title = 	 {{VCR}: A {VDM}-based Software Component Retrieval Tool},
  booktitle = 	 {Proceedings of ICSE-17 Workshop on Formal Methods Application 
                  in Software Engineering Practice},
  year =	 1995,
  address =	 {Seattle}
}

@InCollection{FSS98,
  author =	 {B. Fischer and J.~Schumann and G. Snelting},
  editor =	 {W. Bibel and P. H. Schmitt},
  booktitle = 	 {Automated Deduction -- A Basis for Applications},
  title = 	 {Chapter 11},
  publisher = 	 {Kluwer},
  year = 	 1998,
  pages =	 {265-292}
}

@Unpublished{FoxLon01,
  author = 	 {Maria Fox and Derek Long},
  title = 	 {{PDDL2.1}: An extension to {PDDL} for expressing
                  temporal planning domains},
  note = 	 {Unpublished manuscript},
  year =	 {2001}
}

@InProceedings{FraHofRec04,
  author = 	 {Stephan Frank and Petra Hofstedt and Dirk Reckmann},
  title = 	 {Strategies for the Efficient Solution of Hybrid
                  Constraint Logic Programs},
  booktitle = 	 {Proceedings of 14th Workshop on Logic Programming
                  Environments and 3rd Workshop on Multiparadigm
                  Constraint Programming},
  year =	 2004,
  pages =        {103-118},
  editor =	 {Susana Mu{\~n}oz-Hern{\'a}ndez and Jos{\'e} Manuel G{\'o}mez-Perez
                  and Petra Hofstedt},
  note =	 {Held in conjunction with ICLP04}
}

@Article{FriVel94,
  author = 	 {L. Fribourg and M. Veloso-Peixoto},
  title = 	 {Automates concurrents {\`a} contraintes},
  journal = 	 {Technique et Science Informatiques},
  year = 	 1994,
  volume =	 13,
  number =	 6,
  pages =	 {837-866}
}

@InProceedings{FraHan07,
  author =       {Fr{\"a}nzle, Martin and Hansen, Michael R.},
  title =        {Deciding an Interval Logic with Accumulated
                  Durations},
  booktitle =    {Proceedings of the 13th International Conference on Tools and
                  Algorithms for the Construction and Analysis of
                  Systems},
  year =         2007,
  editor =       {Grumberg, Orna and Huth, Michael},
  series =       {LNCS},
  volume =       4424,
  pages =        {201--215},
  publisher =    {Springer-Verlag},
}

@inproceedings{FraHer03,
  author    = {Martin Fr{\"a}nzle and Christian Herde},
  title     = {Efficient {SAT} Engines for Concise Logics: Accelerating
                  Proof Search for Zero-One Linear Constraint Systems},
  editor    = {Moshe Y. Vardi and
               Andrei Voronkov},
  booktitle = {Proceedings of the 10th International Conference on 
               Logic for Programming, Artificial Intelligence, and Reasoning},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  pages = {302-316}, 
  volume    = {2850},
  year      = {2003}
}

@article{FraHer05entcs,
  author    = {Martin Fr{\"a}nzle and
               Christian Herde},
  title     = {Efficient Proof Engines for Bounded Model Checking of Hybrid
               Systems},
  journal   = {Electronic Notes in Theoretical Computer Science},
  volume    = {133},
  year      = {2005},
  pages     = {119-137}
}

@Article{FraHer06,
  author = 	 {Martin Fr{\"a}nzle and
               Christian Herde},
  title = 	 {{HySAT}: An Efficient Proof Engine for Bounded Model Checking of Hybrid
               Systems},
  journal = 	 {Formal Methods in System Design},
  volume    = {30},
  number    = {3},
  year      = {2007},
  pages     = {179-198}
}

@InProceedings{FraHerRatSchTei06,
  author = 	 {Martin Fr{\"a}nzle and Christian Herde and Stefan
                  Ratschan and Tobias Schubert and Tino Teige},
  title = 	 {Interval Constraint Solving Using Propositional {SAT} Solving Techniques},
  booktitle = 	 {Proceedings of the {CP} 2006 Workshop on the
Integration of {SAT} and {CP} techniques},
  year =	 2006,
  editor =	 {Youssef Hamadi}
}

@Article{FraHerTeiRatSch07,
  author = 	 {Martin Fr{\"a}nzle and Christian Herde and Tino Teige and Stefan
                  Ratschan and Tobias Schubert},
  title = 	 {Efficient Solving of Large Non-linear Arithmetic
                  Constraint Systems with Complex {B}oolean Structure},
  journal = 	 {JSAT Special Issue},
  year = 	 2007,
  note =	 {Submitted}
}

@Unpublished{FraAdeHun05,
  author = 	 {Martin Fr{\"a}nzle and Micha{\"e}l Ad{\'e}la{\"\i}de and Hardi Hungar},
  title = 	 {Compositional Representation of Hybrid Systems via Predicates},
  note = 	 {Have a copy in \texttt{brainstorm/other\_docs/}},
  year =         {2005} 
}

@Article{GabPit02,
  author = 	 {Murdoch Gabbay and Andrew M. Pitts},
  title = 	 {A New Approach to Abstract Syntax with Variable Binding},
  journal = 	 {Formal Aspects of Computing},
  year = 	 2002,
  volume =	 13,
  number =	 {3-5},
  pages =	 {341-363}
}

@inproceedings{GabGlySoe98,
  author    = {Tihomir Gabric and
               Kevin Glynn and
               Harald S{\o}ndergaard},
  title     = {Strictness Analysis as Finite-Domain Constraint Solving},
  booktitle = {Proceedings of the 8th International
               Workshop on Logic Programming Synthesis and Transformation},
  year      = {1998},
  pages     = {255-270},
  publisher =	 {Springer-Verlag},
  series =       {LNCS},
  editor    = {Pierre Flener},
  volume    = {1559}
}

@InProceedings{GalHen04,
  author = 	 {John P. Gallagher and Kim S. Henriksen},
  title = 	 {Abstract Domains Based on Regular Types},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {27-42},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{GanHagNieOliTin04,
  author = 	 {Harald Ganzinger and George Hagen and Robert
                  Nieuwenhuis and Albert Oliveras and Cesare Tinelli},
  title = 	 {$\mathrm{DPLL}(T)$: Fast Decision Procedures},
  booktitle = 	 {Proceedings of the 16th International Conference on 
                  Computer Aided Verification},
  pages =	 {175-188},
  year =	 2004,
  editor =	 {Rajeev Alur and Doron Peled},
  volume =	 3114,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Book{GarJoh79,
  author =	 {Michael R. Garey and David S. Johnson},
  title = 	 {Computers and Intractability. A Guide to the Theory
                  of {NP}-Completeness},
  publisher = 	 {W.H. Freeman and Company},
  year = 	 1979
}

@PhdThesis{Gas95,
  author = 	 {R.~Gasser},
  title = 	 {Harnessing computational resources for efficient
                  exhaustive search},
  school = 	 {ETH Z{\"u}rich},
  year = 	 1995
}

@InProceedings{GasOdd01,
  author =       {Paul Gastin and Denis Oddoux},
  title =        {Fast {LTL} to {B\"{u}chi} Automata Translation},
  BookTitle = "Proceedings of the 13th International Conference on Computer Aided Verification",
  Editor    = "Berry, G. and Comon, H. and Finkel, A.",
  Publisher = "Springer-Verlag",
  Series    = {LNCS},
  volume    = 2102,
  Year      = 2001,
  Pages     = "53--65"
}

@inproceedings{GebSch06,
  author    = {Martin Gebser and
               Torsten Schaub},
  title     = {Tableau Calculi for Answer Set Programming},
  editor    = {Sandro Etalle and
               Miros{\l}aw Truszczy{\'n}ski},
  booktitle     = {Proceedings of the 22nd International Conference on Logic Programming},
  year      = {2006},
  pages     = {11-25},
  publisher = {Springer-Verlag},
  series    = {LNCS}, 
  volume    = {4079}
}

@inproceedings{GebSch07,
  author    = {Martin Gebser and
               Torsten Schaub},
  title     = {Generic Tableaux for Answer Set Programming},
  editor    = {Ver{\'o}nica Dahl and
               Ilkka Niemel{\"a}},
  publisher = {Springer-Verlag},
  volume    = {4670},
  series    = {LNCS},
  booktitle = {Proceedings pf the 23rd International Conference on Logic Programming},
  year      = {2007},
  pages     = {119-133}
}

@article{GelVal05,
  author    = {Jaco Geldenhuys and
               Antti Valmari},
  title     = {More efficient on-the-fly {LTL} verification with {T}arjan's
               algorithm},
  journal   = {Theoretical Computer Science},
  volume    = {345},
  number    = {1},
  year      = {2005},
  pages     = {60-82},
  ee        = {http://dx.doi.org/10.1016/j.tcs.2005.07.004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{GelLif88,
  author    = {Michael Gelfond and
               Vladimir Lifschitz},
  title     = {The Stable Model Semantics for Logic Programming},
  booktitle = {Proceedings of the 5th International Conference and
                  Symposium on Logic Programming},
  editor    = {Robert A. Kowalski and Kenneth A. Bowen},
  year      = {1988},
  pages     = {1070-1080},
  publisher = {MIT Press}
}

@Article{GelLif91,
  author = 	 {Michael Gelfond and
                  Vladimir Lifschitz},
  title = 	 {Classical Negation in Logic Programs and Disjunctive
                  Databases},
  journal = 	 {New Generation Computing},
  year = 	 1991,
  volume =	 9,
  pages =	 {365-385}
}

@article{GelLif93,
  author    = {Michael Gelfond and
               Vladimir Lifschitz},
  title     = {Representing Action and Change by Logic Programs},
  journal   = {Journal of Logic Programming},
  volume    = {17},
  number    = {2/3{\&}4},
  year      = {1993},
  pages     = {301-321}
}

@InProceedings{Gel04,
  author = 	 {Michael Gelfond},
  title = 	 {Answer Set Pogramming and the Design of Deliberative
  Agents},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {19-26},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{GerPelVarWol95,
  author =       {Rob Gerth and
               Doron Peled and
               Moshe Y. Vardi and
               Pierre Wolper},
  title =        {Simple on-the-fly automatic verification of linear temporal logic},
  editor    = {Piotr Dembinski and
               Marek Sredniawa},
  booktitle =    {Proceedings
               of the 15th International Symposium on Protocol Specification, Testing, and Verification},
  pages =        {3--18},
  year =         1996,
  publisher =    {Chapman \& Hall},
  series    = {IFIP Conference Proceedings},
  volume    = {38},
}

@Article{Gib73,
  author = 	 {A. Gibbard},
  title = 	 {Manipulation pf Voting Schemes: A general Result},
  journal = 	 {Econometrica},
  year = 	 1973,
  volume =	 41,
  number =	 4,
  pages =	 {587-601}
}

@PhdThesis{Gir72,
  author = 	 {J.-Y. Girard},
  title = 	 {Interpr{\'e}tation fonctionelle et {\'e}limination des 
                  coupures dans l'arithm{\'e}tique d'ordre sup{\'e}rieure}, 
  school = 	 {Universit{\'e} Paris VII},
  year = 	 1972
}

@article{GiuLieMar06,
  author    = {Enrico Giunchiglia and
               Yuliya Lierler and
               Marco Maratea},
  title     = {Answer Set Programming Based on Propositional Satisfiability},
  journal   = {Journal of Automated Reasoning},
  volume    = {36},
  number    = {4},
  year      = {2006},
  pages     = {345-377}
}

@inproceedings{GiuLieMar04,
  author    = {Enrico Giunchiglia and
               Yuliya Lierler and
               Marco Maratea},
  title     = {A {SAT}-based polynomial space algorithm for answer set programming},
  booktitle = {Proceedings of the 10th 10th International Workshop on Non-Monotonic Reasoning},
  year      = {2004},
  pages     = {189-196},
  editor    = {James P. Delgrande and
               Torsten Schaub}
}

@InProceedings{GiuMar06,
  author = 	 {Enrico Giunchiglia and Marco Maratea},
  title = 	 {Solving Optimization Problems with {DLL}},
  booktitle = 	 {Proceedings of the 17th European Conference on
                  Artificial Intelligence},
  pages =	 {377-381},
  year =	 2006,
  editor =	 {Gerhard Brewka and Silvia Coradeschi and Anna Perini
                  and Paolo Traverso},
  publisher =	 {IOS Press}
}

@InProceedings{GoeSanDri08,
  author = 	 {Robby Goetschalckx and Scott Sanner and Kurt Driessens},
  title = 	 {Reinforcement Learning with the Use of Costly Features},
  booktitle = 	 {Proceedings of the 18th European Conference on
                  Artificial Intelligence},
  pages =	 {777-778},
  year =	 2008,
  editor =	 {Malik Ghallab and Constantine D.~Spyropoulos and
                  Nikos Fakotakis and Nikos Avouris},
  publisher =	 {IOS Press},
  note =         {Poster}
}

@InProceedings{GogKauPapSel95,
  author    = {Goran Gogic and
               Henry A. Kautz and
               Christos H. Papadimitriou and
               Bart Selman},
  title     = {The Comparative Linguistics of Knowledge Representation.},
  booktitle = {Proceedings of the Fourteenth International Joint
               Conference on Artificial Intelligence},
  year      = {1995},
  pages     = {862-869}
}

@InProceedings{GolNov03,
  author    = {E. Goldberg and Y. Novikov},
  title     = {{Verification of Proofs of Unsatisfiability for CNF
Formulas}},
  booktitle = {{Design, Automation, and Test in Europe}},
  year      = {2003}
}

@InProceedings{GraSai97,
  author = 	 {Susanne Graf and Hassen Sa{\"\i}di},
  title = 	 {Construction of abstract state graphs with {PVS}},
  booktitle = 	 {Proceedings of the 9th International Conference on Computer Aided Verification},
  pages =	 {72-83},
  year =	 1997,
  editor =	 {Orna Grumberg},
  volume =	 1254,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Book{GorMel93,
  author =	 {M. J. C. Gordon and T. F. Melham},
  title = 	 {Introduction to HOL},
  publisher = 	 {Cambridge University Press},
  year = 	 1993
}

@inproceedings{GowVru08,
  author    = {Tejaswi Gowda and
               Sarma B. K. Vrudhula},
  title     = {Decomposition based approach for synthesis of multi-level
               threshold logic circuits},
  booktitle = {ASP-DAC},
  year      = {2008},
  pages     = {125-130},
  ee        = {http://dx.doi.org/10.1109/ASPDAC.2008.4483925},
  crossref  = {DBLP:conf/aspdac/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/aspdac/2008,
  title     = {Proceedings of the 13th Asia South Pacific Design Automation
               Conference, ASP-DAC 2008, Seoul, Korea, January 21-24, 2008},
  booktitle = {ASP-DAC},
  publisher = {IEEE},
  year      = {2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{GraHer01,
  author    = {Daniel Cabeza Gras and
               Manuel V. Hermenegildo},
  title     = {Distributed {WWW} Programming using \mbox{({C}iao-)}{P}rolog and the
               {PiLLoW} library},
  journal   = {Theory and Practice of Logic Programming},
  volume    = {1},
  number    = {3},
  year      = {2001},
  pages     = {251-282}
}

@Misc{Gre03,
  author =	 {Harvey J. Greenberg},
  title =	 {Mathematical Programming Glossary Supplement: Convex
                  Cones, Sets, and Functions},
  howpublished = {\url{http://www.cudenver.edu/$\sim$hgreenbe}},
  year =	 2003
}

@InProceedings{GreMazPie06,
  author = 	 {Eric Gr{\'e}goire and Bertrand Mazure and C{\'e}dric Piette},
  title = 	 {Extracting {MUS}es},
  booktitle = 	 {Proceedings of the 17th European Conference on
                  Artificial Intelligence},
  pages =	 {387-391},
  year =	 2006,
  editor =	 {Gerhard Brewka and Silvia Coradeschi and Anna Perini
                  and Paolo Traverso},
  publisher =	 {IOS Press}
}

@inproceedings{GreSchSel06,
  author    = {Susanne Grell and
               Torsten Schaub and
               Joachim Selbig},
  title     = {Modelling Biological Networks by Action Languages Via Answer
               Set Programming},
  editor    = {Sandro Etalle and
               Miros{\l}aw Truszczy{\'n}ski},
  booktitle     = {Proceedings of the 22nd International Conference on Logic Programming},
  year      = {2006},
  pages     = {285-299},
  publisher = {Springer-Verlag},
  series    = {LNCS}, 
  volume    = {4079}
}

@inproceedings{GrobauerM99,
  author    = {Bernd Grobauer and
               Olaf M{\"u}ller},
  title     = {From {I/O} Automata to Timed {I/O} Automata},
  booktitle = {TPHOLs},
  year      = {1999},
  pages     = {273-290},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/1690/16900273.htm},
  crossref  = {DBLP:conf/tphol/1999},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/tphol/1999,
  editor    = {Yves Bertot and
               Gilles Dowek and
               Andr{\'e} Hirschowitz and
               C. Paulin and
               Laurent Th{\'e}ry},
  title     = {Theorem Proving in Higher Order Logics, 12th International
               Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1690},
  year      = {1999},
  isbn      = {3-540-66463-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@PhdThesis{Gro99,
  author = 	 {B. Grobauer},
  title = 	 {Types for Proofs and Programs},
  school = 	 {BRICS},
  year = 	 1999,
  note =	 {Progress Report}
}

@InProceedings{GroZan01,
  author = 	 {Jan Friso Groote and Hans Zantema},
  title = 	 {Resolution and Binary Decision Diagrams Cannot Simulate Each Other Polynomially},
  booktitle = 	 {Proceedings of the 4th International Ershov Memorial Conference},
  year = 	 2001,
  editors =      {Dines Bj{\o}rner and Manfred Broy and Alexandre V. Zamulin},
  pages =	 {33-38},
  volume =	 2244,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Article{GroZan03,
  author = 	 {Jan Friso Groote and Hans Zantema},
  title = 	 {Resolution and Binary Decision Diagrams Cannot Simulate Each Other Polynomially},
  journal = 	 {Discrete Applied Mathematics},
  year = 	 2003,
  volume =	 130,
  number =	 2,
  pages =	 {157-171}
}

@inproceedings{FurKoe05,
  author    = {David Furcy and
               Sven Koenig},
  title     = {Limited Discrepancy Beam Search},
  booktitle = {IJCAI},
  year      = {2005},
  pages     = {125-131},
  ee        = {http://www.ijcai.org/papers/0596.pdf},
  crossref  = {DBLP:conf/ijcai/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/ijcai/2005,
  editor    = {Leslie Pack Kaelbling and
               Alessandro Saffiotti},
  title     = {IJCAI-05, Proceedings of the Nineteenth International Joint
               Conference on Artificial Intelligence, Edinburgh, Scotland,
               UK, July 30-August 5, 2005},
  booktitle = {IJCAI},
  publisher = {Professional Book Center},
  year      = {2005},
  isbn      = {0938075934},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{GupBanMinSimMal07,
  author    = {Gopal Gupta and
               Ajay Bansal and
               Richard Min and
               Luke Simon and
               Ajay Mallya},
  title     = {Coinductive Logic Programming and Its Applications},
  booktitle = {Proceedings of the 23rd International Conference on
                  Logic Programming}, 
  year      = {2007},
  pages     = {27-44},
  series    = {LNCS},
  publisher = {Springer-Verlag},
  volume    = {4670},
  editor    = {Ver{\'o}nica Dahl and
               Ilkka Niemel{\"a}}
}

@InProceedings{GupNau91,
  author = 	 {Naresh Gupta and Dana S. Nau},
  title = 	 {Complexity Results for Blocks-World
                  Planning},
  booktitle = 	 {Proceedings of the 9th National Conference on Artificial Intelligence},
  pages =	 {629-633},
  year =	 1991,
  publisher =	 {AAAI Press / The MIT Press},
  note =	 {Volume 2}
}

@inproceedings{GurKupSomVar03,
  author    = {Sankar Gurumurthy and
               Orna Kupferman and
               Fabio Somenzi and
               Moshe Y. Vardi},
  title     = {On Complementing Nondeterministic {B{\"u}chi} Automata},
  booktitle = {Proceedings of the 12th CHARME Conference},
  year      = {2003},
  pages     = {96-110},
  series    = {LNCS},
  publisher = {Springer-Verlag},
  volume    = {2860},
  editor    = {Daniel Geist and
               Enrico Tronci}
}

@InProceedings{HadHoo07,
  author = 	 {Tarik {Had\v{z}i{\ {\'c}}} and John N. Hooker},
  title = 	 {Cost-bounded Binary Decision Diagrams for 0-1 Programming},
  booktitle = 	 {Proceedings of the 4th International Conference on
        Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems},
  year =	 2007,
  editor =	 {Pascal Van Hentenryck and Laurence Wolsey},
  volume =	 4510,
  pages =        {84-98},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@inproceedings{HarHedBar02,
  author    = {Walter Hartong and
               Lars Hedrich and
               Erich Barke},
  title     = {Model checking algorithms for analog verification},
  booktitle = {Proceedings of the 39th Design Automation Conference},
  year      = {2002},
  publisher = {ACM},
  pages     = {542-547}
}

@Article{HatDan97,
  author = 	 {J. Hatcliff and O. Danvy},
  title = 	 {A Computational Formalization for Partial Evaluation},
  journal = 	 {Mathematical Structures in Computer Science},
  year = 	 1997,
  volume =	 7,
  number =	 5,
  pages =	 {507-542}
}

@Article{Han94,
  author = 	 {M. Hanus},
  title = 	 {The Integration of Functions into Logic
                  Programming: From Theory to Practice},
  journal = 	 {Journal of Logic Programming},
  year = 	 1994,
  volume =	 {19,20},
  pages =	 {583-628}
}

@inproceedings{Has07,
  author    = {Patrik Haslum},
  title     = {Reducing Accidental Complexity in Planning Problems},
  booktitle = {IJCAI},
  year      = {2007},
  pages     = {1898-1903},
  ee        = {http://dli.iiit.ac.in/ijcai/IJCAI-2007/PDF/IJCAI07-306.pdf},
  crossref  = {DBLP:conf/ijcai/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/ijcai/2007,
  editor    = {Manuela M. Veloso},
  title     = {IJCAI 2007, Proceedings of the 20th International Joint
               Conference on Artificial Intelligence, Hyderabad, India,
               January 6-12, 2007},
  booktitle = {IJCAI},
  year      = {2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{heaton97:lopstr, 
author = {Andy  Heaton and Patricia M. Hill
     and Andy King}, 
title = {Analysing Logic Programs with Delay}, 
booktitle = {Proceedings of the 7th
     International Workshop on Logic Program Synthesis and
     Transformation}, 
editor = {Norbert E. Fuchs}, 
series = {LNCS},
volume = {1463},
publisher = {Springer-Verlag}, 
year = 1998 
}

@article{HeaAboCodKin00,
  author    = {Andy Heaton and
               Muhamed Abo-Zaed and
               Michael Codish and
               Andy King},
  title     = {A simple polynomial groundness analysis for logic programs},
  journal   = {Journal of Logic Programming},
  volume    = {45},
  number    = {1-3},
  year      = {2000},
  pages     = {143-156}
}

@InProceedings{HelDom09,
  author = 	 {Malte Helmert and Carmel Domshlak},
  title = 	 {Landmarks, Critical Paths and Abstractions: What's
                  the Difference Anyway?},
  booktitle = 	 {AAAI},
  year =	 2009
}

@Article{HenHoWon98,
  author = 	 {Thomas A. Henzinger and Pei-Hsin Ho and Howard
                  Wong-Toi}, 
  title = 	 {Algorithmic analysis of nonlinear hybrid systems},
  journal = 	 {IEEE Transactions on Automatic Control},
  year = 	 1998,
  volume =	 43,
  number =	 4,
  pages =	 {540-554}
}

@inproceedings{HenManPnu92,
  author    = {Thomas A. Henzinger and
               Zohar Manna and
               Amir Pnueli},
  editor    = {Werner Kuich},
  title     = {What Good Are Digital Clocks?},
  booktitle = {Proceedings of the 19th International
               Colloquium on Automata, Languages and Programming},
  year      = {1992},
  pages     = {545-558},
  series    = {LNCS},
  publisher = {Springer-Verlag},
}

@inproceedings{HenWon96,
  author    = {Thomas A. Henzinger and
               Howard Wong-Toi},
  title     = {Linear Phase-Portrait Approximations for Nonlinear Hybrid
               Systems},
  booktitle = {Proceedings
               of the DIMACS/SYCON Workshop on Hybrid Systems III}, 
  pages     = {377-388},
  publisher = {Springer-Verlag},
  series    = {LNCS}, 
  volume    = {1066},
  year      = {1996}
}

@Article{HeiMicStuYap97,
  author = 	 {N.~Heintze and S.~Michaylov and P.~Stuckey and R.~Yap},
  title = 	 {Meta-programming in {CLP(R)}},
  journal = 	 {Journal of Logic Programming},
  year = 	 1997,
  volume =	 33,
  number =	 3
}

@inproceedings{Hic00,
  author    = {Timothy J. Hickey},
  title     = {Analytic Constraint Solving and Interval Arithmetic},
  booktitle = {Proceedings of Principles of Programming Languages},
  year      = {2000},
  pages     = {338-351}
}

@Misc{HicWit,
  author =	 {Timothy J. Hickey and David K. Wittenberg},
  title =	 {Modeling Hybrid Systems using Analytic Constraint
                  Logic Programming},
  note =	 {Could not find publication data}
}

@InProceedings{hill93,
  author = 	 {Patricia~M.~Hill},
  title = 	 {The Completion of Typed Logic Programs and 
                  {SLDNF}-Resolution},
  booktitle = 	 {Proceedings of the 4th International Conference 
                  on Logic Programming and Automated Reasoning},
  pages =	 {182--193},
  year =	 1993,
  editor =	 {Andrei Voronkov},
  series =	 {LNCS},
  volume =       {698},
  publisher =	 {Springer-Verlag}
}

@Article{Hin69,
  author = 	 {R. Hindley},
  title = 	 {The principal type scheme in an object of combinatory logic},
  journal = 	 {Transactions of the American Mathematical Society},
  year = 	 1969,
  volume =	 146,
  pages =	 {29-60}
}

@InProceedings{HHPW94,
  author = 	 {C. V. Hall and K. Hammond and S. L. {Peyton Jones}
                  and P. Wadler},
  title = 	 {Type Classes in {H}askell},
  booktitle = 	 {Proceedings of the 5th European Symposium on Programming},
  pages =	 {241-256},
  year =	 1994,
  editor =	 {D. Sannella},
  volume =	 788,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Article{HHPW96,
  author = 	 {C. V. Hall and K. Hammond and S. L. {Peyton Jones}
                  and P. Wadler},
  title = 	 {Type Classes in {H}askell},
  journal = 	 {ACM Transactions on Programming Languages and Systems},
  year = 	 1996,
  volume =	 18,
  number =	 2,
  pages =	 {109-138}
}

@InProceedings{HamKnaMer05,
  author =       {Moritz Hammer and Alexander Knapp and Stephan Merz},
  title =        {Truly On-The-Fly {LTL} Model Checking},
  booktitle =    {Proceedings of the 11th International Conference on Tools and Algorithms for the Construction
                  and Analysis of Systems},
  year =         2005,
  editor =       {Nicolas Halbwachs and Lenore Zuck},
  series =       {LNCS}, 
  volume =       3440,
  publisher =    {Springer-Verlag},
  pages =        {191--205}
}

@InProceedings{HasGef00,
  author = 	 {Patrik Haslum and Hector Geffner},
  title = 	 {Admissible Heuristics for Optimal Planning},
  booktitle = 	 {Proceedings of the 5th International Conference on
                  Artificial Intelligence Planning Systems},
  pages =	 {140-149},
  year =	 2000,
  editor =	 {Steve Chien and Subbarao Kambhampati and Craig A. Knoblock},
  organization = {AAAI}
}


@inproceedings{HasBonGef05,
  author    = {Patrik Haslum and
               Blai Bonet and
               Hector Geffner},
  title     = {New Admissible Heuristics for Domain-Independent Planning},
  booktitle     = {Proceedings of the 20th National Conference on Artificial
               Intelligence and the 17th Innovative Applications
               of Artificial Intelligence Conference},
  year      = {2005},
  pages     = {1163-1168},
  publisher = {AAAI Press / The MIT Press},
}

@InProceedings{HelThi98,
  author = 	 {S. Helsen and P. Thiemann},
  title = 	 {Two Flavors of Partial Evaluation},
  booktitle = 	 {Proceedings of ASIAN 98 -- Advances in Computing Science},
  pages =	 {188-205},
  year =	 1998,
  editor =	 {J. Hsiang and A. Ohori},
  volume =	 1538,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{HelThi00,
  author = 	 {S. Helsen and P. Thiemann},
  title = 	 {Fragmental Specialization},
  booktitle = 	 {Semantics, Applications, and Implementation  of
                  Program Generation},
  pages =	 {51-70},
  year =	 2000,
  editor =	 {W. Taha},
  volume =	 1924,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Article{HelThi00-entcs,
  author = 	 {S. Helsen and P. Thiemann},
  title = 	 {Syntactic Type Soundness for the Region Calculus},
  journal = 	 {Electronic Notes in Theorertical Computer Science},
  year = 	 2000,
  volume =	 41,
  number =	 3,
  pages =	 {1-19}
}

@InProceedings{HelThi00-hoots,
  author = 	 {Simon Helsen and Peter Thiemann},
  title = 	 {Syntactic Type Soundness for the Region Calculus},
  crossref =	 {HOOTS2000},
  pages =        {1-20}, 
  year =	 2000
}

@Article{Hen00,
  author = 	 {Thoman A. Henzinger},
  title = 	 {The theory of hybrid automata},
  journal = 	 {Verification of Digital and Hybrid Systems},
  year = 	 2000,
  editor =       {M. K. Inan and R. P. Kurshan},
  series =       {NATO ASI Series F: Computer and Systems Sciences},
  volume =	 170,
  pages =	 {265-292}
}

@Article{HenKopPurVar98,
  author = 	 {Thomas A. Henzinger and Peter W. Kopke and Anuj Puri and Pravin Varaiya},
  title = 	 {What's decidable about hybrid automata?},
  journal = 	 {Journal of Computer and System Sciences},
  year = 	 1998,
  volume =	 57,
  pages =	 {94-124}
}

@Article{HenNicSifYov94,
  author = 	 {Thomas A. Henzinger and Xavier Nicollin and Joseph
                  Sifakis and Sergio Yovine},
  title = 	 {Symbolic Model Checking for Real-Time Systems},
  journal = 	 {Information and Computation},
  year = 	 1994,
  volume =	 111,
  number =	 2,
  pages =	 {193-244}
}

@InProceedings{Hof02,
  author = 	 {J{\"o}rg Hoffmann},
  editor =      "F. Van Harmelen",
  title =        "Extending {FF} to Numerical State Variables",
  booktitle = 	"Proceedings of the 15th European Conference on Artificial
                  Intelligence",
  publisher = 	{Wiley \& Sons},
  pages = "571-575",
  year = 	2002
}

@Article{Hof03,
  author = 	 {J{\"o}rg Hoffmann},
  title = 	 {The Metric-{FF} Planning System: Translating ``Ignoring
                  Delete Lists'' to Numeric State
                  Variables},
  journal = 	 {Journal of Artificial Intelligence Research},
  year = 	 2003,
  volume =	 20,
  pages =	 {291-341}
}

@inproceedings{HofGef03,
  author    = {J{\"o}rg Hoffmann and Hector Geffner},   
  title     = {Branching Matters: Alternative Branching in {G}raphplan},
  editor    = {Enrico Giunchiglia and
               Nicola Muscettola and
               Dana S. Nau},
  booktitle = {Proceedings of the 13th International Conference on Automated
               Planning and Scheduling (ICAPS 2003)},
  publisher = {AAAI},
  pages     = {22-31},
  year      = {2003}
}

@inproceedings{HofKoe99,
  author    = {J{\"o}rg Hoffmann and
               Jana Koehler},
  title     = {A New Method to Index and Query Sets},
  editor    = {Thomas Dean},
  booktitle = {Proceedings of the 16th International Joint Conference
               on Artificial Intelligence},
  year      = {1999},
  pages     = {462-467},
  publisher = {Morgan Kaufmann},
}

@Article{HofNeb01,
  author = 	 {J{\"o}rg Hoffmann and Bernhard Nebel},
  title = 	 {The {FF} Planning System: Fast
       Plan Generation Through Heuristic Search},
  journal = 	 {Journal of Artificial Intelligence Research},
  year = 	 2001,
  volume =	 14,
  pages =	 {253-302}
}
	
@InProceedings{KupHof06,
  author = 	 {Sebastian Kupferschmid and J{\"o}rg Hoffmann},
  title = 	 {An {AI} Planning Heuristics for Directed Model
  Checking, Part {II}: Exploting Automata Locations},
  booktitle = 	 {MoChArt 2006},
  year =	 2006,
  note =	 {Submitted}
}

@inproceedings{KupHofLar08,
  author    = {Sebastian Kupferschmid and
               J{\"o}rg Hoffmann and
               Kim Guldstrand Larsen},
  title     = {Fast Directed Model Checking Via Russian Doll Abstraction},
  booktitle = {TACAS},
  year      = {2008},
  pages     = {203-217},
  ee        = {http://dx.doi.org/10.1007/978-3-540-78800-3_15},
  crossref  = {DBLP:conf/tacas/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/tacas/2008,
  editor    = {C. R. Ramakrishnan and
               Jakob Rehof},
  title     = {Tools and Algorithms for the Construction and Analysis of
               Systems, 14th International Conference, TACAS 2008, Held
               as Part of the Joint European Conferences on Theory and
               Practice of Software, ETAPS 2008, Budapest, Hungary, March
               29-April 6, 2008. Proceedings},
  booktitle = {TACAS},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {4963},
  year      = {2008},
  isbn      = {978-3-540-78799-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{KupWeh11,
  author = 	 {Sebastian Kupferschmid and Martin Wehrle},
  title = 	 {Abstractions and Pattern Databases: The Quest for
Succinctness and Accuracy},
  booktitle = 	 {XXX},
  pages =	 {xxx},
  year =	 2011,
  editor =	 {xxx},
  volume =	 {xxx},
  publisher =	 {xxx}
}

@InProceedings{HolHer99,
  author = 	 {Robert C. Holte and Istv{\'a}n T. Hern{\'a}dv{\"o}lgyi},
  title = 	 {A Space-Time Tradeoff
                  for Memory-Based Heuristics},
  booktitle = 	 {Proceedings of the 16th National Conference on Artificial
                  Intelligence and 11th Conference on Innovative
                  Applications of Artificial Intelligence},
  pages =	 {704-709},
  year =	 1999,
  publisher =	 {AAAI Press / The MIT
                  Press}
}

@Article{HooYan99,
  author = 	 {John N. Hooker and Hong Yan},
  title = 	 {Tight Representations of Logical Constraints
                  as Cardinality Rules},
  journal = 	 {Mathematical Programming},
  year = 	 1999,
  volume =	 85,
  number =       2,
  pages =	 {363-377}
}

@Article{HooOttThoKim00,
  author = 	 {John N. Hooker and G. Ottsson and E.S. Thorsteinsson and
                  H.-J. Kim},
  title = 	 {A scheme for unifying optimization and constraint
                  satisfaction methods},
  journal = 	 {The Knowledge Engineering Review},
  year = 	 2000,
  pages =        {11-30}, 
  volume =	 15
}

@article{Hoo92,
  author    = {John N. Hooker},
  title     = {Generalized Resolution for 0-1 Linear Inequalities},
  journal   = {Annals of Mathematics and Artificial Intelligence},
  volume    = {6},
  number    = {1-3},
  year      = {1992},
  pages     = {271-286}
}

@Book{Hoo00,
  author =	 {John Hooker},
  title = 	 {Logic-Based Methods for Optimization: Combining
                  Optimization and Constraint Satisfaction},
  publisher = 	 {John Wiley},
  year = 	 2000
}

@Proceedings{HOOTS2000,
  title = 	 {ACM Workshop on Higher Order Operational Techniques in Semantics (HOOTS)},
  year = 	 2000,
  volume =       "41(3)",
  editor =	 {Alan Jeffrey},
  series =	 ENTCS,
  address =	 {Montreal, Canada},
  month =	 sep,
  publisher =	 {Elsevier Science},
  url =		 {http://www.elsevier.nl/locate/entcs/volume41.html}
}

@Unpublished{HelThi00-unpublished,
  author = 	 {S. Helsen and P. Thiemann},
  title = 	 {Polymorphic Specialization for Polymorphic Programming
  Languages},
  note = 	 {Preliminary Work for \cite{HelThi03}},
  year =	 2000
}

@Article{HelThi03,
  author = 	 {S. Helsen and P. Thiemann},
  title = 	 {Polymorphic Specialization for ML},
  journal = 	 {ACM Transactions on Programming Languages and Systems},
  year = 	 2003,
  note =	 {To appear}
}


@inproceedings{HenJhaMajMcM04,
  author    = {Thomas A. Henzinger and
               Ranjit Jhala and
               Rupak Majumdar and
               Kenneth L. McMillan},
  title     = {Abstractions from proofs},
  editor    = {Neil D. Jones and
               Xavier Leroy},
  booktitle = {Proceedings of the 31st Symposium on
               Principles of Programming Languages},
  year      = {2004},
  pages     = {232-244},
  publisher = {ACM},
}

@InProceedings{HenKupQad98,
  author    = {Thomas A. Henzinger and Orna Kupferman and Shaz
                  Qadeer}, 
  editor    = {Alan J. Hu and
               Moshe Y. Vardi},
  title     = {From Pre-historic to
                  Post-modern Symbolic Model Checking},
  booktitle = {Proceedings of the 10th International Conference on Computer Aided Verification},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {1427},
  year      = {1998},
  pages     = {195-206}
}

@InProceedings{Her00,
  author = 	 {Istv{\'a}n T. Hern{\'a}dv{\"o}lgyi},
  title = 	 {Automatic Generation of Memory Based Search
                  Heuristics},
  booktitle = 	 {Proceedings of the 17th National Conference on Artificial
                  Intelligence and 12th Conference on on Innovative
                  Applications of Artificial Intelligence},
  pages =	 1103,
  year =	 2000,
  publisher =	 {AAAI Press / The
                  MIT Press}
}

@inproceedings{HerHol00,
  author    = {Istv{\'a}n T. Hern{\'a}dv{\"o}lgyi and
               Robert C. Holte},
  title     = {Experiments with Automatically Created Memory-Based Heuristics},
  editor    = {Berthe Y. Choueiry and
               Toby Walsh},
  booktitle = {Proceedings of the 4th International
               Symposium on Abstraction, Reformulation, and
               Approximation}, 
  year      = {2000},
  pages     = {281-290},
  publisher = {Springer-Verlag},
  series    = {LNCS}
}

@Book{HirSmaDev04,
  author =	 {Morris W. Hirsch,Stephen Smale,Robert L. Devaney},
  title = 	 {Differential equations, dynamical systems, and an introduction to chaos},
  publisher = 	 {Elsevier},
  year = 	 2004
}

@Article{HisPai00,
  author = 	 {Ian A. Hiskens and M.A. Pai},
  title = 	 {Trajectory sensitivity analysis of hybrid systems},
  journal = 	 {IEEE Transactions on Circuits and Systems I: Fundamental Theory and Applications},
  year = 	 2000,
  volume =	 47,
  number =	 2,
  pages =	 {204-220}
}

@Misc{Hof05,
  author =	 {J{\"o}rg Hoffmann},
  title =	 {Search Methods for Transition Systems},
  note =	 {Lecture slides: \href{other_docs/hoffmann/6-patterndb.pdf}{6-patterndb.pdf}},
  year =         {2005}
}

@Article{Hof05jair,
  author = 	 {J{\"o}rg Hoffmann},
  title = 	 {Where Ignoring Delete Lists Works: Local Search Topology
    in Planning Benchmarks},
  journal = 	 {Journal of Artificial Intelligence Research},
  year = 	 2005,
  note =	 {Available from \url{http://www.mpi-sb.mpg.de/$\sim$hoffmann/papers/jair05b.ps.gz}}
}

@inproceedings{HolPerZimMac96,
  author    = {Robert C. Holte and
               M. B. Perez and
               Robert M. Zimmer and
               Alan J. MacDonald},
  title     = {Hierarchical A$^*$: Searching Abstraction Hierarchies Efficiently},
  booktitle = {Proceedings of the 13th National Conference on Artificial
Intelligence and 8th Innovative Applications of Artificial
Intelligence Conference},
  year      = {1996},
  pages     = {530-535},
  volume    = {1}, 
  publisher = {AAAI Press / The MIT Press}
}

@Book{Hol90,
  author =	 {Gerard J. Holzmann},
  title = 	 {Design and Validation of Computer Protocols},
  publisher = 	 {Prentice Hall},
  year = 	 1990
}

@article{Hol97,
  author    = {Gerard J. Holzmann},
  title     = {The Model Checker {SPIN}},
  journal   = {IEEE Transactions on Software Engineering},
  volume    = {23},
  number    = {5},
  year      = {1997},
  pages     = {279-295}
}

@article{HosTakKanYaj97,
  author    = {Kazuhisa Hosaka and
               Yasuhiko Takenaga and
               T. Kaneda and
               Shuzo Yajima},
  title     = {Size of Ordered Binary Decision Diagrams Representing Threshold
               Functions},
  journal   = {Theoretical Computer Science},
  volume    = {180},
  number    = {1-2},
  year      = {1997},
  pages     = {47-60}
}

@Book{Hu65,
  author =	 {Sze-Tsen Hu},
  title = 	 {Threshold Logic},
  publisher = 	 {University of California Press},
  year = 	 1965
}

@TechReport{Hun00,
  author = 	 {Thomas S. Hune},
  title = 	 {Modeling a Language for Embedded Systems in Timed Automata},
  institution =  {BRICS},
  year = 	 2000,
  number =	 {RS-00-17}
}

@inproceedings{IglGupPonRanMil01,
  author    = {Juan Raymundo Iglesias and
               Gopal Gupta and
               Enrico Pontelli and
               Desh Ranjan and
               Brook Milligan},
  title     = {Interoperability between Bioinformatics Tools: A Logic Programming
               Approach},
  editor    = {I. V. Ramakrishnan},
  booktitle = {Proceedings of the 3rd International
               Symposium on Practical Aspects of Declarative Languages},
  year      = {2001},
  pages     = {153-168},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {1990}
}

@InProceedings{JacMis01,
  author = 	 {James Jacob and Alan Mishchenko},
  title = 	 {Unate decomposition of {B}oolean
                  functions},
  booktitle = 	 {Proceedings of IWLS},
  pages =	 {66-71},
  year =	 {2001},
  note = {Available from
                  \url{http://www-cad.eecs.berkeley.edu/$\sim$alanmi/publications/2001/iwls01\_unate.pdf}}
}

@techreport{Jan03,
    address = {Espoo, Finland},
    author = {Tomi Janhunen},
    institution = {Helsinki University of Technology, Laboratory for Theoretical Computer Science},
    month = {November},
    number = {A82},
    pages = {88},
    title = {Translatability and Intranslatability Results for Certain Classes of Logic Programs},
    type = {Research Report},
    year = {2003},
}

@article{janowska06,
  author    = {A. Janowska and
               P. Janowski},
  title     = {{Slicing of Timed Automata with Discrete Data}},
  journal   = {Fundamenta Informaticae},
  volume    = {72},
  number    = {1-3},
  year      = {2006}
}

@InProceedings{JGBDM90,
  author = 	 {N. D. Jones and C. K. Gomard and A. Bondorf 
                  and O. Danvy and T. Mogensen},
  title = 	 {A Self-applicable Partial Evaluator for the Lambda Caluculus},
  booktitle = 	 {Proceedings of the IEEE Computer Society International 
                  Conference on Computer Languages},
  pages =	 {49-58},
  year =	 1990
}

@Book{JGS93,
  author =	 {N. D. Jones and C. K. Gomard and P. Sestoft},
  title = 	 {Partial Evaluation and Automatic Program Generation},
  publisher = 	 {Prentice Hall},
  year = 	 1993
}

@InProceedings{Jon90,
  author = 	 {N. D. Jones},
  editor =       {M. Paterson},
  title = 	 {Partial Evaluation, Self-Application and Types},
  booktitle = 	 {Colloquium on Automata, Languages and Programming},
  pages =	 {639-659},
  year =	 1990,
  volume =	 443,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{Jon92,
  author = 	 {M. P. Jones},
  editor =       {B. Krieg-Br{\"u}ckner},
  title = 	 {A Theory of Qualified Types},
  booktitle = 	 {European Symposium on Programming},
  pages =        {287-306},
  year =	 1992,
  number =	 {582},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{Jon00,
  author = 	 {M. P. Jones},
  title = 	 {Type Classes with Functional Dependencies},
  booktitle = 	 {Proceedings of the 9th European Symposium on Programming},
  pages =	 {230-244},
  year =	 2000,
  editor =	 {Gert Smolka},
  volume =	 1782,
  series =	 {LNCS},
  publisher =	 {Springer}
}

@Article{JonJFP,
  author = 	 {M. P. Jones},
  title = 	 {Typing {H}askell in {H}askell},
  journal = 	 {Journal of Functional Programming},
  year = 	 2002,
  note =	 {Under consideration.}
}

@InProceedings{Kae88,
  author = 	 {S. Kaes},
  title = 	 {Parametric Polymorphism},
  booktitle = 	 {Proceedings of the 2nd European Symposium on Programming},
  year =	 1988,
  volume =	 300,
  series =	 {LNCS}
}

@inproceedings{KarDom09,
  author    = {Erez Karpas and
               Carmel Domshlak},
  title     = {Cost-Optimal Planning with Landmarks},
  booktitle = {IJCAI},
  year      = {2009},
  pages     = {1728-1733},
  ee        = {http://ijcai.org/papers09/Papers/IJCAI09-288.pdf},
  crossref  = {DBLP:conf/ijcai/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/ijcai/2009,
  editor    = {Craig Boutilier},
  title     = {IJCAI 2009, Proceedings of the 21st International Joint
               Conference on Artificial Intelligence, Pasadena, California,
               USA, July 11-17, 2009},
  booktitle = {IJCAI},
  year      = {2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{katoen,
  author = {P.R. D'Argenio and J.P. Katoen and Th.C. Ruys and G.J. Tretmans},
  title = {{The Bounded Retransmission Protocol must be on time!}},
  booktitle = {TACAS},
  year      = {1997}
}

@InProceedings{KauSel92,
  author = 	 {Henry A. Kautz and Bart Selman},
  title = 	 {Planning as Satisfiability},
  booktitle = 	 {Proceedings of the 10th European Conference
                  on Artificial Intelligence},
  pages =	 {359-363},
  year =	 1992,
  editor =	 {Bernd Neumann},
  publisher =	 {Wiley \& Sons}
}

@InProceedings{KauSel96,
  author = 	 {Henry A. Kautz and Bart Selman},
  title = 	 {Pushing the Envelope: Planning,
                  Propositional Logic and Stochastic
                  Search},
  booktitle = 	 {Proceedings of the 13th National Conference on
                  Artificial Intelligence and 8th Innovative
                  Applications of Artificial Intelligence Conference},
  pages =	 {1194-1201},
  year =	 1996,
  publisher =	 {MIT Press}
}

@InProceedings{KauMcASel96,
  author = 	 {Henry A. Kautz and David A. McAllester and Bart Selman},
  title = 	 {Encoding Plans in Propositional Logic},
  booktitle = 	 {Proceedings of the 5th International Conference on
                  Principles of Knowledge Representation and Reasoning},
  pages =	 {374-384},
  year =	 1996,
  editor =	 {Luigia Carlucci Aiello and Jon Doyle and Stuart C. Shapiro},
  publisher =	 {Morgan Kaufmann}
}

@inproceedings{KayLynSegVaa03,
  author    = {Dilsun Kirli Kaynar and
               Nancy A. Lynch and
               Roberto Segala and
               Frits W. Vaandrager},
  title     = {Timed {I/O} Automata: A Mathematical Framework for Modeling
               and Analyzing Real-Time Systems},
  booktitle = {Proceedings of the 24th IEEE Real-Time Systems Symposium},
  year      = {2003},
  pages     = {166-177},
  publisher = {IEEE Computer Society}
}

@Book{Kha02,
  author =	 {Hassan K. Khalil},
  title = 	 {Nonlinear System},
  publisher = 	 {Prentice Hall},
  year = 	 2002,
  edition =	 3
}

@inproceedings{KimEspKum05,
  author    = {Jongwoo Kim and
               Joel M. Esposito and
               Vijay Kumar},
  title     = {An RRT-Based Algorithm for Testing and Validating Multi-Robot
               Controllers},
  editor    = {Sebastian Thrun and
               Gaurav S. Sukhatme and
               Stefan Schaal},
  booktitle = {Proceedings of Robotics: Science and Systems I},
  year      = {2005},
  pages     = {249-256},
  publisher = {The MIT Press}
}

@inproceedings{Kla04,
  author    = {Felix Klaedtke},
  title     = {On the Automata Size for Presburger Arithmetic.},
  booktitle = {Proceedings of the 19th IEEE Symposium on Logic in Computer Science},
  year      = {2004},
  pages     = {110-119},
  publisher = {IEEE Computer Society}
}

@InProceedings{KlaRatShe07,
  author = 	 {Felix Klaedtke and Stefan Ratschan and Zhikun She},
  title = 	 {Language-Based Abstraction Refinement for Hybrid
                  System Verification},
  booktitle = 	 {Submitted to VMCAI07},
  year =	 2007,
  editor =	 {Andreas Podelski},
  volume =	 {???},
  series =	 {LNCS},
  pages = {??-??},
  publisher =	 {Springer-Verlag}
}

@Book{Kle52,
  author =	 {Stephen Cole Kleene},
  title = 	 {Introduction to Metamathematics},
  publisher = 	 {North-Holland},
  year = 	 1980,
  note =         {First published in 1952}
}

@Article{KleMar75,
  author = 	 {Daniel Kleitman and George Markowsky},
  title = 	 {On {D}edekind's problem: the number of isotone
                  {B}oolean functions. {II}},
  journal = 	 {Transactions of the American Mathematical Society},
  year = 	 1975,
  volume =	 213,
  pages =	 {373-390}
}

@article{Kno94,
  author    = {Craig A. Knoblock},
  title     = {Automatically Generating Abstractions for Planning},
  journal   = {Artif. Intell.},
  volume    = {68},
  number    = {2},
  year      = {1994},
  pages     = {243-302},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{KnuMorPra77,
  author = 	 {D. E. Knuth and J. H. Morris and V. R. Pratt},
  title = 	 {Fast Pattern Matching in Strings},
  journal = 	 {SIAM},
  year = 	 1977,
  volume =	 6,
  number =	 2,
  pages =	 {323-350}
}

@InProceedings{Koe98,
  author = 	 {Jana Koehler},
  title = 	 {Solving Complex Planning Tasks Through Extraction of
                  Subproblems},
  booktitle = 	 {Proceedings
                  of the 4th International Conference on Artificial
                  Intelligence Planning Systems},
  pages =	 {62-69},
  year =	 1998,
  editor =	 {Reid G. Simmons and Manuela M. Veloso and Stephen Smith},
  publisher =	 {AAAI}
}

@InProceedings{KoeHof00,
  author = 	 {Jana Koehler and J{\"o}rg Hoffmann},
  title = 	 {On the instantiation of {ADL} operators involving
                  arbitrary first-order formulas},
  booktitle = 	 {Proceedings of the ECAI-00 Workshop on New Results
                  in Planning, Scheduling and Design},
  year =	 2000
}

@inproceedings{KoeNebHofDim97,
  author    = {Jana Koehler and Bernhard Nebel and J{\"o}rg Hoffmann and Yannis
                  Dimopoulos},
  editor    = {Sam Steel and
               Rachid Alami},
  title     = {On the instantiation of {ADL} operators involving
                  arbitrary first-order formulas},
  booktitle = {Proceedings of the 4th European Conference on Planning},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {1348},
  year      = {1997},
  pages     = {273-285}
}

@Article{KolLewTor03,
  author = 	 {Tamara G. Kolda and Robert Michael Lewis and Virginia Torczon},
  title = 	 {Optimization by direct search: new perspectives on some classical and modern methods},
  journal = 	 {SIAM Review},
  year = 	 2003,
  volume =	 45,
  number =	 3,
  pages =	 {385-482}
}

@InProceedings{Kor97,
  author = 	 {Richard E. Korf},
  title = 	 {Finding Optimal Solutions to {R}ubik's {C}ube Using Pattern Databases},
  booktitle = 	 {Proceedings of the 14th National Conference on Artificial
                  Intelligence and 9th Innovative Applications of
                  Artificial Intelligence Conference},
  pages =	 {700-705},
  year =	 1997,
  publisher =	 {MIT Press}
}

@Article{KorFel02,
  author = 	 {Richard E. Korf and Ariel Felner},
  title = 	 {Disjoint pattern database
                  heuristic},
  journal = 	 {Artificial Intelligence},
  year = 	 2002,
  volume =	 134,
  number =	 {1-2},
  pages =	 {9-22}
}

@inproceedings{KorRei98,
  author    = {Richard E. Korf and
               Michael Reid},
  title     = {Complexity Analysis of Admissible Heuristic Search},
  booktitle = {Proceedings of the 15th National Conference on Artificial
                  Intelligence and 10th Innovative Applications of
                  Artificial Intelligence Conference},
  year      = {1998},
  pages     = {305-310},
  publisher = {AAAI Press / The MIT Press}
}
	
@InProceedings{KorTay96,
  author = 	 {Richard E. Korf and Larry A. Taylor},
  title = 	 {Finding Optimal Solutions to
                  the Twenty-Four Puzzle},
  booktitle = 	 {Proceedings of the 13th National Conference on Artificial
                  Intelligence and 8th Innovative Applications of
                  Artificial Intelligence Conference},
  pages =	 {1202-1207},
  year =	 1996,
  publisher =    {AAAI Press / The MIT Press},
  volume =	 2
}

@Book{KorVyg02,
  author =	 {B. Korte and J. Vygen},
  title = 	 {Combinatorial Optimization: Theory and Algorithms},
  publisher = 	 {Springer-Verlag},
  year = 	 2002
}

@Article{KovBroTar07,
  author = 	 {Andr{\'a}s Kov{\'a}cs and Kenneth N. Brown and S. Armagan Tarim},
  title = 	 {An Efficient {MIP} Model for the Capacitated
                  Lot-sizing and Scheduling Problem with
                  Sequence-dependent Setups},
  journal = 	 {International Journal of Production Economics},
  year = 	 {2006?},
  note =	 {Submitted}
}

@Unpublished{Kra07,
  author = 	 {Alexander Krauss},
  title = 	 {Defining Recursive Functions in {I}sabelle/{HOL}},
  note = 	 {Available from \url{http://isabelle.in.tum.de/doc/functions.pdf}},
  year =         {2007}
}

@inproceedings{KriPelOldBae99,
  author    = {Bernd Krieg-Br{\"u}ckner and
               Jan Peleska and
               Ernst-R{\"u}diger Olderog and
               Alexander Baer},
  title     = {The {UniForM} Workbench, a Universal Development Environment
               for Formal Methods},
  editor    = {Jeannette M. Wing and
               Jim Woodcock and
               Jim Davies},
  booktitle = {Proceedings of the World Congress on Formal Methods
               in the Development of Computing Systems},
  year      = {1999},
  pages     = {1186-1205},
  publisher = {Springer-Verlag},
  volume    = {1709},
  series    = {LNCS}
}

@article{KupVar01,
  author    = {Orna Kupferman and
               Moshe Y. Vardi},
  title     = {Weak alternating automata are not that weak},
  journal   = {ACM Trans. Comput. Log.},
  volume    = {2},
  number    = {3},
  year      = {2001},
  pages     = {408-429},
  ee        = {http://doi.acm.org/10.1145/377978.377993},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{KupVar05,
  author    = {Orna Kupferman and
               Moshe Y. Vardi},
  title     = {Complementation Constructions for Nondeterministic Automata
               on Infinite Words},
  booktitle = {Proceedings of the 11th International Conference on  
               Tools and Algorithms for the Construction and Analysis of
               Systems},
  year      = {2005},
  pages     = {206-221},
  series    = {LNCS},
  publisher = {Springer-Verlag},
  editor    = {Nicolas Halbwachs and
               Lenore D. Zuck},
  volume    = {3440}
}

@inproceedings{Rao04,
  author    = {M. R. K. {Krishna Rao}},
  title     = {Input-Termination of Logic Programs},
  booktitle = {Proceedings of the 14th International
               Symposium on Logic Based Program Synthesis and
                  Transformation}, 
  editor    = {Sandro Etalle},
  year      = {2005},
  pages     = {215-230},
  series    = {LNCS},
  publisher = {Springer-Verlag},
  volume    = {3573},
}

@InProceedings{KroWeeZha08,
  author = 	 {{\SortNoop{Krogt}}{van der} Krogt, Roman   and 
                  {\SortNoop{Weerdt}}de Weerdt, Mathijs  and
                  Zhang, Yingqian},
  title = 	 {Of Mechanism Design and Multiagent Planning},
  booktitle = 	 {Proceedings of the 18th European Conference on
                  Artificial Intelligence},
  pages =	 {423-427},
  year =	 2008,
  editor =	 {Malik Ghallab and Constantine D.~Spyropoulos and
                  Nikos Fakotakis and Nikos Avouris},
  publisher =	 {IOS Press}
}

@proceedings{DBLP:conf/ecai/2008,
  editor    = {Malik Ghallab and
               Constantine D. Spyropoulos and
               Nikos Fakotakis and
               Nikolaos M. Avouris},
  title     = {ECAI 2008 - 18th European Conference on Artificial Intelligence,
               Patras, Greece, July 21-25, 2008, Proceedings},
  booktitle = {ECAI},
  publisher = {IOS Press},
  series    = {Frontiers in Artificial Intelligence and Applications},
  volume    = {178},
  year      = {2008},
  isbn      = {978-1-58603-891-5},
  ee        = {http://www.booksonline.iospress.nl/Content/View.aspx?piid=9905},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{KupHofDieBeh05,
  author = 	 {Sebastian Kupferschmid and J{\"o}rg Hoffmann and Henning
                  Dierks and Gerd Behrmann},
  title = 	 {Enhancing {UPPAAL} with Automatically Generated Heuristics:
                  First Results},
  booktitle = 	 {Proceedings of CAV},
  year =	 2005,
  note =	 {Submitted}
}

@InProceedings{KupHofDieBeh06-tacas,
  author = 	 {Sebastian Kupferschmid and J{\"o}rg Hoffmann and Henning
                  Dierks and Gerd Behrmann},
  title = 	 {Boosting {UPPAAL} by an {AI} Planning Heuristic},
  booktitle = 	 {Proceedings of TACAS},
  year =	 2006,
  note =	 {Submitted}
}

@InProceedings{KupHofDieBeh06-spin,
  author = 	 {Sebastian Kupferschmid and J{\"o}rg Hoffmann and Henning
                  Dierks and Gerd Behrmann},
  title = 	 {Adapting an {AI} Planning Heuristic for Directed
                  Model Checking},
  booktitle = {Proceedings of the 13th International SPIN Workshop on Model Checking Software},
  year      = {2006},
  pages     = {35-52},
  editor    = {Antti Valmari},
  series    = {LNCS},
  publisher = {Springer-Verlag},
  volume    = {3925}
}

@InProceedings{KupDraHofFinDiePodBeh07,
  author = 	 {Sebastian Kupferschmid and Klaus Dr{\"a}ger and J{\"o}rg
                  Hoffmann and Bernd Finkbeiner and Henning Dierks and Andreas Podelski and Gerd Behrmann},
  title = 	 {\textsc{Uppaal/DMC} -- {A}bstraction-based Heuristics for Directed Model Checking},
  booktitle = 	 {Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  pages =	 {679-682},
  year =	 2007,
  editor =	 {Orna Grumberg and Michael Huth},
  volume =	 {4424},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Manual{Lam11,
  title = 	 {Refinement Framework Userguide},
  author =	 {Peter Lammich},
  organization = {Technische Universit{\"a}t M{\"u}nchen},
  year =	 2011
}

@Unpublished{LamTue12,
  author = 	 {Peter Lammich and Thomas Tuerk},
  title = 	 {Applying Data Refinement for Monadic Programs to
  Hopcroft's Algorithm},
  note = 	 {Submitted to ITP 2012},
  year =         {2012}
}

@inproceedings{LarBurRumHol10,
  author    = {Bradford John Larsen and
               Ethan Burns and
               Wheeler Ruml and
               Robert Holte},
  title     = {Searching Without a Heuristic: Efficient Use of Abstraction},
  booktitle = {AAAI},
  year      = {2010},
  ee        = {http://www.aaai.org/ocs/index.php/AAAI/AAAI10/paper/view/1893},
  crossref  = {DBLP:conf/aaai/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/aaai/2010,
  editor    = {Maria Fox and
               David Poole},
  title     = {Proceedings of the Twenty-Fourth AAAI Conference on Artificial
               Intelligence, AAAI 2010, Atlanta, Georgia, USA, July 11-15,
               2010},
  booktitle = {AAAI},
  publisher = {AAAI Press},
  year      = {2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{LarLarPetYi97,
  title =     {Efficient Verification of Real-time Systems: Compact
                  Data Structure and State-space Reduction},
  author =    {K.G. Larsen and F. Larsson and P. Pettersson and W. Yi},
  booktitle     = {Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS
               '97)},
  publisher = {IEEE Computer Society},
  year      = {1997},
  pages = {14-24}
}

@Article{LarPetYi97,
  author = 	 {Kim Guldstrand Larsen and Paul Pettersson and Wang Yi},
  title = 	 {{UPPAAL} in a Nutshell},
  journal = 	 {International Journal on Software Tools for Technology Transfer},
  year = 	 1997,
  volume =	 1,
  number =	 {1-2},
  pages =	 {134-152}
}

@article{LeoPfeFabEitGotPerSca06,
  author    = {Nicola Leone and
               Gerald Pfeifer and
               Wolfgang Faber and
               Thomas Eiter and
               Georg Gottlob and
               Simona Perri and
               Francesco Scarcello},
  title     = {The {DLV} system for knowledge representation and reasoning},
  journal   = {ACM Transactions on Computational Logic},
  volume    = {7},
  number    = {3},
  year      = {2006},
  pages     = {499-562}
}

@InProceedings{LewSchBec07,
  author = 	 {Matthew Lewis and Tobias Schubert and Bernd Becker},
  title = 	 {Multithreaded {SAT} Solving},
  booktitle = 	 {Proceedings of the 12th Asia and South Pacific Design Automation Conference},
  year =	 2007
}

@InProceedings{LiAnb97,
  author = 	 {Chu Min Li and Anbulagan},
  title = 	 {Heuristics Based on Unit Propagation
                  for Satisfiability Problems},
  booktitle = 	 {Proceedings of the 15th International Joint Conference on Artificial Intelligence},
  pages =	 {366-371},
  year =	 1997,
  volume =	 1
}

@article{Lif02,
  author    = {Vladimir Lifschitz},
  title     = {Answer Set Programming and Plan Generation},
  journal   = {Artificial Intelligence},
  volume    = {138},
  number    = {1-2},
  year      = {2002},
  pages     = {39-54}
}

@Article{LinChuLiu87,
  author = 	 {F. J. Lin and P. M Chu and M. T. Liu},
  title = 	 {Protocol Verification Using Reachability Analysis: the state space explosion problem and relief strategies},
  journal = 	 {ACM SIGCOMM},
  year = 	 1987,
  pages =	 {126-135}
}

@inproceedings{LinZhaHer06,
  author    = {Zhijun Lin and
               Yuanlin Zhang and
               Hector Hernandez},
  title     = {Fast {SAT}-based Answer Set Solver},
  booktitle = {Proceedings on the 21st National Conference on Artificial
               Intelligence and the 18th Innovative Applications
               of Artificial Intelligence Conference},
  year      = {2006},
  publisher = {AAAI Press}
}

@article{LinZha04,
  author    = {Fangzhen Lin and
               Yuting Zhao},
  title     = {{ASSAT}: computing answer sets of a logic program by {SAT} solvers},
  journal   = {Artificial Intelligence},
  volume    = {157},
  number    = {1-2},
  year      = {2004},
  pages     = {115-137}
}

@inproceedings{LinAngKon02,
  author    = {Thomas Linke and
               Christian Anger and
               Kathrin Konczak},
  title     = {More on {noMoRe}},
  editor    = {Sergio Flesca and
               Sergio Greco and
               Nicola Leone and
               Giovambattista Ianni},
  booktitle = {Proceedings of the European Conference on Logics in
                  Artificial Intelligence}, 
  year      = {2002},
  pages     = {468-480},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {2424}
}

@InProceedings{Loc08,
  author = 	 {Andreas Lochbihler},
  title = 	 {Type Safe Nondeterminism -- A Formal Semantics of {J}ava},
  booktitle = 	 {Proceedings of FOOL},
  year =	 2008
}

@Article{LonFox99,
  author = 	 {Derek Long and Maria Fox},
  title = 	 {Efficient Implementation of the Plan Graph in
                  {STAN}},
  journal = 	 {Journal of Artificial Intelligence Reasoning},
  year = 	 1999,
  volume =	 10,
  pages =	 {87-115}
}

@Article{LooWei93,
  author =       {R\"udiger Loos and Volker Weispfenning},
  title =        {Applying Linear Quantifier Elimination},
  journal =      {The Computer Journal},
  year =         1993,
  volume =       36,
  number =       5,
  pages =        {450--462}
}

@InProceedings{Lop08,
  author = 	 {Carlos Linares L{\'o}pez},
  title = 	 {Multi-valued Pattern Databases},
  booktitle = 	 {Proceedings of the 18th European Conference on
                  Artificial Intelligence},
  pages =	 {540-544},
  year =	 2008,
  editor =	 {Malik Ghallab and Constantine D.~Spyropoulos and
                  Nikos Fakotakis and Nikos Avouris},
  publisher =	 {IOS Press}
}

@inproceedings{LomWozZbr07,
  author    = {Alessio Lomuscio and
               Bozena Wozna and
               Andrzej Zbrzezny},
  editor =       {Stefan Edelkamp and Alessio Lomuscio},   
  title     = {Bounded Model Checking Real-Time Multi-agent Systems with
               Clock Differences: Theory and Implementation},
  booktitle = {Post-Proceedings of the 4th (2006) Workshop on Model Checking
                  and Artificial Intelligence},
  year      = {2007},
  pages     = {95-112},
  series =	 {LNCS},
  volume    =    {4428},
  publisher =	 {Springer-Verlag}
}

@article{LomPenWoz07,
  author    = {Alessio Lomuscio and
               Wojciech Penczek and
               Bozena Wozna},
  title     = {Bounded model checking for knowledge and real time},
  journal   = {Artificial Intelligence},
  volume    = {171},
  number    = {16-17},
  year      = {2007},
  pages     = {1011-1038}
}

@article{Lux07,
  author    = {Ulrike von Luxburg},
  title     = {A Tutorial on Spectral Clustering},
  journal   = {Statistics and Computing},
  volume    = {17},
  number    = {4},
  year      = {2007},
  pages     = {395-416}
}

@inproceedings{LynSegVaa01,
  author    = {Nancy A. Lynch and
               Roberto Segala and
               Frits W. Vaandrager},
  title     = {Hybrid {I/O} Automata Revisited},
  booktitle = {Proceedings of the 4th International
               Workshop on Hybrid Systems: Computation and Control},
  year      = {2001},
  pages     = {403-417},
  editor    = {Maria Domenica Di Benedetto and
               Alberto L. Sangiovanni-Vincentelli},
  series    = {LNCS},
  publisher = {Springer-Verlag},
  volume    = {2034},
}

@inproceedings{LynSegVaaWei95,
  author    = {Nancy A. Lynch and
               Roberto Segala and
               Frits W. Vaandrager and
               H. B. Weinberg},
  title     = {Hybrid {I/O} Automata},
  editor    = {Rajeev Alur and
               Thomas A. Henzinger and
               Eduardo D. Sontag},
  booktitle = {Hybrid Systems},
  publisher = {Springer},
  volume    = {1066},
  series    = {LNCS}, 
  year      = {1995},
  pages     = {496-510}
}

@Book{ManPnu95,
  author =	 {Z. Manna and A. Pnueli},
  title = 	 {Temporal Verification of Reactive Systems: Safety},
  publisher = 	 {Springer-Verlag},
  year = 	 1995
}

@Article{ManRou06,
   author = {Vasco M. Manquinho and Olivier Roussel},
   title = {The First Evaluation of Pseudo-{B}oolean Solvers ({PB}'05)},
   journal = {Journal on Satisfiability, Boolean Modeling and Computation},
   volume = {2},
   pages = {103-143},
   year = {2006}
}


@InProceedings{Mar99,
  author = 	 {Jo{\~a}o P. {Marques Silva}},
  title = 	 {The Impact of Branching Heuristics in
                  Propositional Satisfiability Algorithms},
  booktitle = 	 {Proceedings of the 9th Portuguese Conference on
                  Artificial Intelligence},
  pages =	 {62-74},
  year =	 1999,
  editor =	 {Pedro Barahona and Jos{\'e} J{\'u}lio Alferes},
  volume =	 1695,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Article{MarSak99,
  author = 	 {Jo{\~a}o P. {Marques Silva} and Karem A. Sakallah},
  title = 	 {{GRASP}: A Search Algorithm
                  for Propositional Satisfiability},
  journal = 	 {IEEE
                  Transactions on Computers},
  year = 	 1999,
  volume =	 48,
  number =	 5,
  pages =	 {506-521}
}

@inproceedings{MarKin97,
  author    = {Jonathan C. Martin and
               Andy King},
  editor    = {Michel Bidoit and
               Max Dauchet},
  title     = {Generating Efficient, Terminating Logic Programs},
  booktitle = {Proceedings of the 7th International Joint Conference
                  on Theory and Practice of Software Development},
  year      = {1997},
  pages     = {273-284},
  series =    {LNCS},
  volume    = {1214},
  publisher = {Springer-Verlag}
}


@Article{McD00,
  author = 	 {Drew V. McDermott},
  title = 	 {The 1998 {AI} Planning Systems Competition},
  journal = 	 {AI Magazine},
  year = 	 2000,
  volume =	 21,
  number =	 2,
  pages =	 {35-55}
}

@InProceedings{McM-cav03,
  author = 	 {Kenneth L. McMillan},
  title = 	 {Interpolation and {SAT}-Based Model Checking},
  booktitle = 	 {Proceedings of the 15th International Conference on
                  Computer Aided Verification},
  pages =	 {1-13},
  year =	 2003,
  editor =	 {Warren A. Hunt Jr. and
               Fabio Somenzi},
  volume =	 2725,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{McM-tacas04,
  author    = {Kenneth L. McMillan},
  title     = {An Interpolating Theorem Prover}, 
  editor    = {Kurt Jensen and
               Andreas Podelski},
  booktitle = {Proceedings of the 10th International Conference on 
               Tools and Algorithms for the Construction and Analysis of Systems},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {2988},
  year      = {2004},
  pages     = {16-30}
}

@InProceedings{McM-tacas05,
  author = 	 {Kenneth L. McMillan},
  title = 	 {Applications of {Craig} Interpolants in Model
                  Checking},
  booktitle = 	 {Proceedings of the 11th International Conference on 
                  Tools and Algorithms for the Construction and Analysis of
                  Systems},
  pages =	 {1-12},
  year =	 2005,
  editor =	 {Nicolas Halbwachs and
               Lenore D. Zuck},
  volume =	 3440,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{McMAml-tacas03,
  author = 	 {Kenneth L. McMillan and Nina Amla},
  title = 	 {Automatic Abstraction without Counterexamples},
  booktitle = 	 {Proceedings of the 9th International Conference on 
                  Tools and Algorithms for the Construction and Analysis of
                  Systems},
  pages =	 {2-17},
  year =	 2003,
  editor =	 {Hubert Garavel and John Hatcliff},
  volume =	 2619,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@inproceedings{ManGun12,
  author    = {William Mansky and
               Elsa L. Gunter},
  title     = {Using Locales to Define a Rely-Guarantee Temporal Logic},
  booktitle = {ITP},
  year      = {2012},
  pages     = {299-314},
  ee        = {http://dx.doi.org/10.1007/978-3-642-32347-8_20},
  crossref  = {DBLP:conf/itp/2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/itp/2012,
  editor    = {Lennart Beringer and
               Amy P. Felty},
  title     = {Interactive Theorem Proving - Third International Conference,
               ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings},
  booktitle = {ITP},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7406},
  year      = {2012},
  isbn      = {978-3-642-32346-1},
  ee        = {http://dx.doi.org/10.1007/978-3-642-32347-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Book{MeiThe98,
  author =	 {Christoph Meinel and Thorsten Theobald},
  title = 	 {Algorithms and Data Structures in VLSI Design: OBDD - Foundations and Applications},
  publisher = 	 {Springer},
  year = 	 1998
}

@Book{KroMer08,
  author =       {Fred Kr{\"o}ger and Stephan Merz},
  title =        {Temporal Logic and State Systems},
  publisher = 	 {Springer},
  year = 	 2008,
  series = 	 {Texts in Theoretical Computer Science},
  address = 	 {Berlin, Germany},
}

@InBook{MerKro08,
  author =	 {Stephan Merz and Fred Kr{\"o}ger},
  title = 	 {Expressiveness of Propositional Linear Temporal
                  Logics (Chapter Title)},
  chapter = 	 4,
  publisher = 	 {??},
  year = 	 2008
}

@inproceedings{Mer00,
  author    = {Stephan Merz},
  editor    = {Mark Aagaard and
               John Harrison},
  title     = {Weak Alternating Automata in {I}sabelle/{HOL}},
  booktitle = {Proceedings of the 13th International
               Conference on Theorem Proving in Higher Order Logics},
  year      = {2000},
  pages     = {424-441},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {1869}
}

%Hat auch mal unter dem Namen "Elements of Model Checking" kursiert
@InCollection{Mer08,
 author =      {Stephan Merz},
 title =       {An Introduction to Model Checking},
 booktitle =   {Modeling and Verification of Real-Time Systems},
 pages =       {81--115},
 publisher = {ISTE Publishing},
 year =        2008,
 editor =      {S. Merz and N. Navet},
 address =     {London, UK}}

@InCollection{Mer01,
 author =      {Stephan Merz},
 title =       {Model Checking: A Tutorial Overview},
 booktitle =   {Modeling and Verification of Parallel Processes},
 pages =       {3--38},
 publisher =   {Springer-Verlag},
 year =        2001,
 editor =      {F. Cassez et al.},
 volume =      2067,
 series =      {Lecture Notes in Computer Science},
 address =     {Berlin}}

@Book{Mil89,
  author =	 {Robin Milner},
  title = 	 {Communication and Concurrency},
  publisher = 	 {Prentice Hall},
  year = 	 1989
}

@inproceedings{Min99,
  author    = {Marius Minea},
  title     = {Partial Order Reduction for Model Checking of Timed Automata.},
  booktitle = {Proceedings of the 10th
                  International Conference on Concurrency Theory},
  year      = {1999},
  pages     = {431-446},
  editor    = {Jos C. M. Baeten and
               Sjouke Mauw},
  series    =	 {LNCS},
  publisher =	 {Springer-Verlag},
  volume    = {1664}
}

@Book{Mit96,
  author =	 {J. C. Mitchell},
  title = 	 {Foundations for Programing Languages},
  publisher = 	 {The MIT Press},
  year = 	 1996
}

@inproceedings{MiyHay84,
  author    = {Satoru Miyano and
               Takeshi Hayashi},
  title     = {Alternating Finite Automata on omega-Words},
  booktitle = {CAAP},
  year      = {1984},
  pages     = {195-210},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{MoeRueSor02,
  author    = {M. Oliver M{\"o}ller and
               Harald Rue{\ss} and
               Maria Sorea},
  title     = {Predicate Abstraction for Dense Real-Time Systems},
  journal   = {Electronic Notes on Theoretical Computer Science},
  volume    = {65},
  number    = {6},
  year      = {2002}
}

@InProceedings{MonSauLam04,
  author = 	 {Eric Monfroy and Fr{\'e}d{\'e}ric Saubion and Tony Lambert},
  title = 	 {On Hybridization of Local Search and Constraint
  Propagation},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {299-313},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Book{Moo66,
  author =	 {Ramon E. Moore},
  title = 	 {Interval Analysis},
  publisher = 	 {Prentice Hall},
  year = 	 1966
}

@inproceedings{MorMar08,
  author    = {Ant{\'o}nio Morgado and
               Jo{\~a}o P. {Marques Silva}},
  title     = {A Pseudo-Boolean Solution to the Maximum Quartet Consistency
               Problem},
  booktitle = {Proceedings of the Workshop on
Constraint Based Methods for Bioinformatics},
  volume    = {abs/0805.0202},
  year      = {2008},
  note      = {Avaliable via Corr, http://arxiv.org/abs/0805.0202}
}




@InProceedings{MosMadZhaZhaMal01,
  author = 	 {Matthew W. Moskewicz and Conor F. Madigan and Ying
                  Zhao and Lintao Zhang and
                  Sharad Malik},
  title = 	 {Engineering an Efficient {SAT}
                  Solver},
  booktitle = 	 {Proceedings of the 38th Design Automation Conference},
  pages =	 {530-535},
  year =	 2001,
  publisher =	 {ACM}
}

@InProceedings{MouRueSor02,
  author = 	 {Leonardo {Mendon{\c c}a de Moura} and Harald Rue{\ss} and Maria
                  Sorea},
  title = 	 {Lazy Theorem
                  Proving for Bounded Model Checking over Infinite
                  Domains},
  booktitle = 	 {Proceedings of the 18th International Conference
               on Automated Deduction},
  pages =	 {438-455},
  year =	 2002,
  editor =	 {Andrei Voronkov},
  volume =	 2392,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@inproceedings{MouRueSor03,
  author    = {Leonardo {Mendon\c{c}a de Moura} and
               Harald Rue{\ss} and
               Maria Sorea},
  editor    = {Hunt, Jr., Warren and
               Fabio Somenzi},
  title     = {Bounded Model Checking and Induction: From Refutation to
               Verification (Extended Abstract, Category {A})},
  booktitle     = {Proceedings of the 15th International Conference
               on Computer Aided Verification},
  year      = {2003},
  pages     = {14-26},
  publisher = {Springer-Verlag},
  volume    = {2725},
  series    = {LNCS} 
}

@inproceedings{MikucionisLRNSPPH10,
  author    = {Marius Mikucionis and
               Kim Guldstrand Larsen and
               Jacob Illum Rasmussen and
               Brian Nielsen and
               Arne Skou and
               Steen Ulrik Palm and
               Jan Storbank Pedersen and
               Poul Hougaard},
  title     = {Schedulability Analysis Using Uppaal: Herschel-Planck Case
               Study},
  booktitle = {ISoLA (2)},
  year      = {2010},
  pages     = {175-190},
  ee        = {http://dx.doi.org/10.1007/978-3-642-16561-0_21},
  crossref  = {DBLP:conf/isola/2010-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/isola/2010-2,
  editor    = {Tiziana Margaria and
               Bernhard Steffen},
  title     = {Leveraging Applications of Formal Methods, Verification,
               and Validation - 4th International Symposium on Leveraging
               Applications, ISoLA 2010, Heraklion, Crete, Greece, October
               18-21, 2010, Proceedings, Part II},
  booktitle = {ISoLA (2)},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6416},
  year      = {2010},
  isbn      = {978-3-642-16560-3},
  ee        = {http://dx.doi.org/10.1007/978-3-642-16561-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{MugDeR94,
  author    = {Stephen Muggleton and
               Luc {De Raedt}},
  title     = {Inductive Logic Programming: Theory and Methods},
  journal   = {Journal of Logic Programming},
  volume    = {19/20},
  year      = {1994},
  pages     = {629-679}
}

@InProceedings{MukPod99,
  author    = {Supratik Mukhopadhyay and Andreas Podelski}, 
  editor    = {C. Pandu Rangan and
               Venkatesh Raman and
               R. Ramanujam},
  title     = {Beyond Region Graphs:
               Symbolic Forward Analysis of Timed Automata},
  booktitle = {Proceedings of the 19th Conference on Foundations 
               of Software Technology and Theoretical Computer Science},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {1738},
  year      = {1999},
  pages     = {232-244}    
}

@InProceedings{MukPod00,
  author    = {Supratik Mukhopadhyay and Andreas Podelski}, 
  editor    = {John W. Lloyd and
               Ver{\'o}nica Dahl and
               Ulrich Furbach and
               Manfred Kerber and
               Kung-Kiu Lau and
               Catuscia Palamidessi and
               Lu\'{\i}s Moniz Pereira and
               Yehoshua Sagiv and
               Peter J. Stuckey},
  title     = {Model Checking for Timed
               Logic Processes},
  booktitle = {Proceedings of the 1st International Conference 
               on Computational Logic},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {1861},
  year      = {2000},
  pages     = {598-612}    
}

@InProceedings{MukPod01-padl,
  author    = {Supratik Mukhopadhyay and Andreas Podelski},   
  editor    = {I. V. Ramakrishnan},
  title     = {Constraint Database
                  Models Characterizing Timed Bisimilarity},
  booktitle = {Proceedings of the 3rd International
               Symposium on Practical Aspects of Declarative Languages}, 
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {1990},
  year      = {2001},
  pages     = {245-258}
}

@InProceedings{MukPod01-ersh,
  author    = {Supratik Mukhopadhyay and Andreas Podelski},
  editor    = {Dines Bj{\o}rner and
               Manfred Broy and
               Alexandre V. Zamulin},
  title     = {Accurate Widenings
               and Boundedness Properties of Timed Systems},
  booktitle = {Revised Papers of the 4th International Andrei
               Ershov Memorial Conference Perspectives of System Informatics},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {2244},
  year      = {2001},
  pages     = {79-94}
}

@InCollection{Muk97,
  author = 	 {Madhavan Mukund},
  title = 	 {Linear-Time Temporal Logic and {B}{\"u}chi Automata},
  booktitle = 	 {Winter School on Logic and Computer Science},
  publisher =	 {Indian Statistical Institute},
  year =	 1997,
  address =	 {Calcutta},
  month =	 {January},
  note =	 {Tutorial talk}
}

@article{MulSch87,
  author    = {David E. Muller and
               Paul E. Schupp},
  title     = {Alternating Automata on Infinite Trees},
  journal   = {Theoretical Computer Science},
  volume    = {54},
  year      = {1987},
  pages     = {267-276}
}

@InProceedings{MulSaoSch86,
  author = 	 {David E. Muller and Ahmed Saoudi and Paul E. Schnupp},
  title = 	 {Alternating Automata. {T}he Weak Monadic Theory of the Tree, and its Complexity},
  booktitle = 	 {Proceedings of the 13th International Colloquium on
                  Automata, Languages and Programming (ICALP)},
  pages =	 {275-283},
  year =	 1986,
  editor =	 {Laurent Kott},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@inproceedings{MunMarMor04,
  title =     {Constructive Intensional Negation},
  author =    {Susana Mu{\~n}oz-Hern{\'a}ndez and Julio Mari{\~n}o and Juan Jos{\'e} Moreno-Navarro},
  editor    = {Yukiyoshi Kameyama and
               Peter J. Stuckey},
  booktitle  = {Proceedings of the 7th International Symposium on 
                Functional and Logic Programming}, 
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {2998},
  year      = {2004}
}

@Article{MW97,
  author = 	 {A. {Moormann Zaremski} and J.~M. Wing},
  title = 	 {Specification Matching of Software Components},
  journal = 	 {ACM Transactions on Software Engineering and Methodology},
  year = 	 1997,
  volume =	 6,
  number =	 4,
  pages =	 {333-369}
}

@inproceedings{MunMor03,
  title =     {A Real Implementation for Constructive Negation},
  author =    {Susana Mu{\~n}oz-Hern{\'a}ndez and Juan Jos{\'e} Moreno-Navarro},
  editor    = {Catuscia Palamidessi},
  booktitle = {Proceedings of the 19th International Conference on
                 Logic Programming},
  publisher = {Springer-Verlag},
  series    = {LNCS},           
  volume    = {2916},
  pages     = {496-497},
  year      = {2003}
}

@inproceedings{MunMor04,
  title =     {Implementation Results in Classical Constructive Negation},
  author =    {Susana Mu{\~n}oz-Hern{\'a}ndez and Juan Jos{\'e} Moreno-Navarro},
  editor    = {Bart Demoen and Vladimir Lifschitz},
  booktitle = {Proceedings of the 20th International Conference on
                 Logic Programming},
  publisher = {Springer-Verlag},
  series    = {LNCS},           
  volume    = {3132},
  pages     = {284-298},
  year      = {2004}
}

@Book{Mur71,
  author =	 {Saburo Muroga},
  title = 	 {Threshold Logic and its Applications},
  publisher = 	 {Wiley-Interscience},
  year = 	 1971
}

@inproceedings{Myc84,
     author = "Alan Mycroft",
     title = "Polymorphic Type Schemes and Recursive Definitions",
     booktitle = "Proceedings of the 6th International Symposium on Programming",
     publisher = "Springer-Verlag",
     series = {LNCS},
     volume = {167},
  editor    = {Manfred Paul and
               Bernard Robinet},
     year = 1984,
     pages = "217--228"
     }

@inproceedings{NahDan07,
  author    = {Tarik Nahhal and
               Thao Dang},
  title     = {Test Coverage for Continuous and Hybrid Systems},
  booktitle = {CAV},
  year      = {2007},
  pages     = {449-462},
  ee        = {http://dx.doi.org/10.1007/978-3-540-73368-3_47},
  crossref  = {DBLP:conf/cav/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/cav/2007,
  editor    = {Werner Damm and
               Holger Hermanns},
  title     = {Computer Aided Verification, 19th International Conference,
               CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings},
  booktitle = {CAV},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4590},
  year      = {2007},
  isbn      = {978-3-540-73367-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{Neb00,
  author    = {Bernhard Nebel},
  title     = {On the Compilability and Expressive Power of Propositional
               Planning Formalisms},
  journal   = {Journal Artificial Intelligence Research},
  volume    = {12},
  year      = {2000},
  pages     = {271-315}
}

@InProceedings{NebDimKoe97,
  author = 	 {Bernhard Nebel and Yannis Dimopoulos and Jana Koehler},
  title = 	 {Ignoring Irrelevant
                  Facts and Operators in Plan Generation},
  booktitle = 	 {Proceedings of the 4th European Conference on Planning},
  pages =	 {338-350},
  year =	 1997,
  editor =	 {Sam Steel and Rachid Alami},
  volume =	 1348,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{NeuThi02,
  author = 	 {M. Neubauer and P. Thiemann},
  title = 	 {Type Classes with more Higher-Order Polymorphism},
  booktitle = 	 {Proceedings of the 7th International Conference on
                  Functional Programming },
  pages =	 {179-190},
  year =	 2002,
  number =	 {37(9)},
  series =	 {SIGPLAN Notices},
  organization = {ACM}
}

@InProceedings{NeuThiGasSpe02,
  author = 	 {M. Neubauer and P. Thiemann and M. Gasbichler and
                  M. Sperber},
  title = 	 {Functional Logic Overloading},
  booktitle = 	 {Conference Record of the 29th Symposium on Principles of Programming Languages},
  pages =	 {233-244},
  year =	 2002,
  series =	 {SIGPLAN/SIGACT},
  organization = {ACM}
}

@Unpublished{Nip99,
  author = 	 {T. Nipkow},
  title = 	 {Towards Verified Bytecode Verifiers},
  note = 	 {Unpublished},
  year =	 1999
}

@InProceedings{NipSne91,
  author = 	 {T. Nipkow and G. Snelting},
  title = 	 {Type Classes and Overloading Resolution via Order-Sorted Unification},
  booktitle = 	 {Functional Programming Languages and Computer Architecture},
  year =	 1991,
  volume =	 523,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@INCOLLECTION{Nis07,
  author = {N. Nisan},
  title = {Introduction to Mechanism Design (for Computer Scientists)},
  booktitle = {Algorithmic Game Theory},
  publisher = {Cambridge University Press},
  year = {2007},
  pages = {209--242}
}

@InProceedings{NogAbrDav04,
  author = 	 {Vitor Beires Nogueira and Salvador Abreu and Gabriel
                  David},
  title = 	 {Towards Temporal Reasoning in Constraint Contextual
                  Logic Programming},
  booktitle = 	 {Proceedings of 14th Workshop on Logic Programming
                  Environments and 3rd Workshop on Multiparadigm
                  Constraint Programming},
  year =	 2004,
  pages =        {119-131},
  editor =	 {Susana Mu{\~n}oz-Hern{\'a}ndez and Jos{\'e} Manuel G{\'o}mez-Perez
                  and Petra Hofstedt},
  note =	 {Held in conjunction with ICLP04}
}

@inproceedings{Non00,
  author    = {Andreas Nonnengart},
  title     = {Hybrid Systems Verification by Location Elimination},
  booktitle = {Proceedings of the 3rd International
               Workshop on Hybrid Systems},
  year      = {2000},
  pages     = {352-365},
  editor    = {Nancy A. Lynch and
               Bruce H. Krogh},
  volume    = {1790},
  publisher = {Springer-Verlag},
  series    = {LNCS}
}

@InProceedings{NopSch04,
  author = 	 {Tobias Nopper and Christoph Scholl},
  title = 	 {Symbolic Model Checking for Incomplete Designs},
  booktitle = 	 {Proceedings of the 5th International Conference on
                  Formal Methods in  Computer-Aided Design},
  year =	 2004,
  editor =	 {Alan Hu and Andrew Martin},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag},
  note =	 {To appear}
}

@InProceedings{OliSifYov94,
  author = 	 {Alfredo Olivero and Joseph Sifakis and Sergio Yovine},
  title = 	 {Using Abstractions for
                  the Verification of Linear Hybrid Systems},
  booktitle = 	 {Proceedings of the 6th International Conference on
                  Computer Aided Verification},
  pages =	 {81-94},
  year =	 1994,
  editor =	 {David L. Dill},
  volume =	 818,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Book{OttWie02,
  author =	 {Thomas Ottmann and Peter Widmayer},
  title = 	 {Algorithmen und Datenstrukturen},
  publisher = 	 {Spektrum Akademischer Verlag},
  year = 	 2002,
  edition =	 4
}

@inproceedings{PalGopTra10,
  author    = {Ashok Kumar Palaniswamy and
               Manoj Kumar Goparaju and
               Spyros Tragoudas},
  title     = {Scalable identification of threshold logic functions},
  booktitle = {ACM Great Lakes Symposium on VLSI},
  year      = {2010},
  pages     = {269-274},
  ee        = {http://doi.acm.org/10.1145/1785481.1785545},
  crossref  = {DBLP:conf/glvlsi/2010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/glvlsi/2010,
  editor    = {R. Iris Bahar and
               Fabrizio Lombardi and
               David Atienza and
               Erik Brunvand},
  title     = {Proceedings of the 20th ACM Great Lakes Symposium on VLSI
               2009, Providence, Rhode Island, USA, May 16-18 2010},
  booktitle = {ACM Great Lakes Symposium on VLSI},
  publisher = {ACM},
  year      = {2010},
  isbn      = {978-1-4503-0012-4},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{PalTra12,
  author    = {Ashok Kumar Palaniswamy and
               Spyros Tragoudas},
  title     = {A scalable threshold logic synthesis method using ZBDDs},
  booktitle = {ACM Great Lakes Symposium on VLSI},
  year      = {2012},
  pages     = {307-310},
  ee        = {http://doi.acm.org/10.1145/2206781.2206856},
  crossref  = {DBLP:conf/glvlsi/2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/glvlsi/2012,
  editor    = {Erik Brunvard and
               Ken Stevens and
               Joseph R. Cavallaro and
               Tong Zhang},
  title     = {Great Lakes Symposium on VLSI 2012, GLSVLSI'12, Salt Lake
               Cit, UT, USA, May 3-4, 2012},
  booktitle = {ACM Great Lakes Symposium on VLSI},
  publisher = {ACM},
  year      = {2012},
  isbn      = {978-1-4503-1244-8},
  ee        = {http://dl.acm.org/citation.cfm?id=2206781},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DalDovFog04,
  author    = {Alessandro {Dal Pal{\`u}} and
               Agostino Dovier and
               Federico Fogolari},
  title     = {Constraint Logic Programming Approach to Protein Structure
               Prediction},
  journal   = {BMC Bioinformatics},
  volume    = {5},
  year      = {2004},
  pages     = {186}
}

@Article{DalDovPon10,
  author = 	 {Alessandro {Dal Pal{\`u}} and
               Agostino Dovier and Enrico Pontelli},
  title = 	 {Computing Approximate Solutions of the Protein Structure Determination Problem using Global Constraints on Discrete Crystal Lattices},
  journal = 	 {International Journal of Data Mining and Bioinformatics},
  year = 	 2010,
  volume =	 4,
  number =	 1
}

@Article{DalDovPon07,
  author = 	 {Alessandro {Dal Pal{\`u}} and
               Agostino Dovier and Enrico Pontelli},
  title = 	 {A Constraint Solver for Discrete Lattices, its Parallelization, and Application to Protein Structure Prediction},
  journal = 	 {Software -- Practice and Experience},
  year = 	 2007,
  volume =	 37,
  number =	 13,
  pages =        {1405-1449}
}


@Article{PapYan91,
  author = 	 {Christos H. Papadimitriou and Mihalis Yannakakis},
  title = 	 {Shortest Paths Without a Map},
  journal = 	 {Theoretical Computer Science},
  year = 	 1991,
  volume =	 84,
  number =	 1,
  pages =	 {127-150}
}

@InProceedings{PasSch07,
  author = 	 {Adrian Paschke and Michael Schr{\"o}der},
  title = 	 {Inductive Logic Programming for Bioinformatics in {P}rova},
  booktitle = 	 {Proceedings of the VLDB Workshop on Data Mining in Bioinformatics},
  year =	 2007,
  editor =	 {Mehmet M. Dalkilic and
David P. Kreiland
Sun Kimand
Jiong Yang}
}

@InProceedings{PavTasAdaHan08,
  author = 	 {Ioannis Pavlidis and Dimitris Tasoulis and Niall
                  M. Adams and David J. Hand},
  title = 	 {Dynamic Multi-Armed Bandit with Covariates},
  booktitle = 	 {Proceedings of the 18th European Conference on
                  Artificial Intelligence},
  pages =	 {777-778},
  year =	 2008,
  editor =	 {Malik Ghallab and Constantine D.~Spyropoulos and
                  Nikos Fakotakis and Nikos Avouris},
  publisher =	 {IOS Press},
  note =         {Poster}
}

@Book{Pea85,
  author =	 {Judea Pearl},
  title = 	 {Heuristic},
  publisher = 	 {Addison-Wesley},
  year = 	 1985
}

@article{PedRug04,
  author    = {Dino Pedreschi and
               Salvatore Ruggieri},
  title     = {Bounded Nondeterminism of Logic Programs},
  journal   = {Annals of Mathematics and Artificial Intelligence},
  volume    = {42},
  number    = {4},
  year      = {2004},
  pages     = {313-343},
  publisher = {Springer-Verlag}
}

@Article{PlaGre86,
  author = 	 {David A. Plaisted and Steven Greenbaum},
  title = 	 {A Structure Preserving Clause Form Translation},
  journal = 	 {Journal of Symbolic Computation},
  year = 	 1986,
  volume =	 2,
  number =	 3,
  pages =	 {293-304}
}

@InProceedings{PlaKavVar07,
  author = 	 {Erion Plaku and Lydia Kavraki and Moshe Vardi},
  title = 	 {Hybrid Systems: From Verification to Falsification},
  booktitle = 	 {Proceedings of the 19th International Conference on 
                  Computer Aided Verification},
  pages =	 {463-476},
  year =	 2007,
  editor =	 {Holger Hermanns and Werner Damm},
  volume =	 {4590},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Article{Plo75,
  author = 	 {G. Plotkin},
  title = 	 {Call-by-name, call-by-value, and the $\lambda$-calculus},
  journal = 	 {Theretical Computer Science},
  year = 	 1975,
  volume =	 1,
  pages =	 {125-159}
}

@Article{Pnu81,
  author = 	 {Amir Pnueli},
  title = 	 {The temporal semantics of concurrent programs},
  journal = 	 {Theoretical Computer Science},
  year = 	 1981,
  volume =	 13,
  pages =	 {45-60}
}

@InProceedings{Pod00,
  author    = {Andreas Podelski},
  editor    = {Jens Palsberg},
  title     = {Model Checking as Constraint Solving},
  booktitle = {Proceedings of the 7th International Symposium on Static Analysis},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {1824},
  year      = {2000},
  pages     = {22-37}
}


@InProceedings{Pod03,
  author = 	 {Andreas Podelski},
  title = 	 {Software Model Checking with Abstraction Refinement},
  booktitle = 	 {Proceedings of the 4th International Conference on 
                  Verification, Model Checking, and Abstract Interpretation},
  pages =	 {1-3},
  year =	 2003,
  editor =	 {Lenore D. Zuck and
               Paul C. Attie and
               Agostino Cortesi and
               Supratik Mukhopadhyay},
  volume =	 2575,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{PodChaMul99,
  author    = {Andreas Podelski and Witold Charatonik and Martin M{\"u}ller},
  editor    = {S. Doaitse Swierstra},
  title     = {Set-Based Failure Analysis for Logic Programs and 
               Concurrent Constraint Programs},
  booktitle = {Proceedings of the 8th European Symposium on
               Programming Languages and Systems},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {1576},
  year      = {1999},
  pages     = {177-192}
}

 @InProceedings{PodRyb04,
  author = 	 {Andreas Podelski and Andrey Rybalchenko},
  title = 	 {Transition Invariants},
  booktitle = 	 {Proceedings of the 19th Symposium on Logic in Computer Science},
  pages =	 {32-41},
  year =	 2004,
  organization = {IEEE}
}

@InProceedings{PodRyb05,
  author = 	 {Andreas Podelski and Andrey Rybalchenko},
  editor =       {Mart{\'\i}n Abadi},
  title = 	 {Transition Predicates and Fair Termination},
  booktitle = 	 {Conference Record of the 32nd ACM Symposium on Principles of Programming Languages},
  pages =	 {132-144},
  year =	 2005
}

@inproceedings{PodRyb07,
   author    = {Andreas Podelski and Andrey Rybalchenko},
   title     = {{ARMC}: the Logical Choice for Software Model Checking with 
                Abstraction Refinement},
   editor    = {Michael Hanus},
   booktitle = {Proceedings of the 9th International Symposium on
                Practical Aspects of Declarative Languages},
   year      = {2007},
   pages     = {245--259},
   publisher = {Springer-Verlag},
   volume    = {4354},
   series    = {LNCS},
}

@InProceedings{PodWag05,
  author = 	 {Andreas Podelski and Silke Wagner},
  title = 	 {Model Checking for Stability Properties of Linear
                  Hybrid Systems},
  booktitle = 	 {Submitted to ICALP},
  year =	 2005
}

@TechReport{Pol96,
  author = 	 {R. Pollack},
  title = 	 {What we learn from formal checking, part I: {H}ow to
                  believe a machine-checked proof},
  institution =  {BRICS autumn school on verification},
  year = 	 1996,
  number =	 {Notes Series NS-96-8},
  address =	 {BRICS, Department of Computer Science, University of
                  Aarhus}
}

@proceedings{PolPeaHeyRuc07,
  editor    = {Axel Polleres and
               David Pearce and
               Stijn Heymans and
               Edna Ruckhaus},
  title     = {Proceedings of the ICLP'07 Workshop on Applications of Logic
               Programming to the Web, {S}emantic {W}eb and {S}emantic {W}eb Services,
               ALPSWS 2007, Porto, Portugal, September 13th, 2007},
  publisher = {CEUR-WS.org},
  series    = {CEUR Workshop Proceedings},
  volume    = {287},
  year      = {2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{PonSon06,
  author    = {Enrico Pontelli and
               Tran Cao Son},
  title     = {{\it Justifications} for Logic Programs Under Answer Set
               Semantics},
  editor    = {Sandro Etalle and
               Miros{\l}aw Truszczy{\'n}ski},
  booktitle     = {Proceedings of the 22nd International Conference on Logic Programming},
  year      = {2006},
  pages     = {196-210},
  publisher = {Springer-Verlag},
  series    = {LNCS}, 
  volume    = {4079}
}

@InProceedings{PraPapPar02,
  author = 	 {S. Prajna, A. Papachristodoulou, P. A. Parrilo.},
  title = 	 {Introducing {SOSTOOLS}: A General Purpose Sum of Squares Programming Solver},
  booktitle =	 {CDC'02},
  year =	 2002
}

@inproceedings{PraRan05,
  author    = {Stephen Prajna and
               Anders Rantzer},
  title     = {Primal-Dual Tests for Safety and Reachability},
  booktitle = {Proceedings of the 8th International Workshop on Hybrid
                  Systems: Computation and Control}, 
  year      = {2005},
  pages     = {542-556},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag},
  volume    = {3414},
  editor    = {Manfred Morari and
               Lothar Thiele}
}

@Book{PreFlaTeuVet92,
  author =	 {Press and Flannery and Teukolski and Vetterling},
  title = 	 {Numerical Recipes in C},
  publisher = 	 {Cambridge University Press},
  year = 	 1992
}

@InProceedings{QiaNym04,
  author = 	 {Kairong Qian and
               Albert Nymeyer},
  title = 	 {Guided Invariant Model Checking Based on Abstraction and
               Symbolic Pattern Databases},
  booktitle =  {Proceedings of the 10th International Conference on
                Tools and Algorithms for the Construction and Analysis of
                Systems},
  pages =	 {497-511},
  year =	 2004,
  editor =	 {Kurt Jensen and
               Andreas Podelski},
  volume =	 2988,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@inproceedings{QiaNym04-atva,
  author    = {Kairong Qian and
               Albert Nymeyer},
  title     = {Abstraction-Based Model Checking Using Heuristical Refinement},
  editor    = {Farn Wang},
  booktitle = {Proceedings of the 2nd  International Conference on Automated Technology for Verification and Analysis},
  year      = {2004},
  pages     = {165-178},
  series    = {LNCS},
  volume    = {3299},
  publisher = {Springer-Verlag}
}

@Article{RacBadBenCaiLegPas11,
  author = 	 {Jean-Baptiste Raclet and Eric Badouel and Albert Benveniste and Beno{\^\i}t Caillaud and
Axel Legay and Roberto Passerone},
  title = 	 {A Modal Interface Theory for
Component-based Design},
  journal = 	 {Fundamenta Informaticae},
  year = 	 2011,
  volume =	 108,
  number =	 {1-2}
}

@InProceedings{RatShe05,
  author = 	 {Stefan Ratschan and Zhikun She},
  editor =       {Manfred Morari and Lothar Thiele},
  title = 	 {Safety Verification of Hybrid Systems by Constraint Propagation Based Abstraction Refinement},
  booktitle = 	 {Hybrid Systems: Computation and Control},
  year =	 2005,
  series =	 {LNCS},  
  volume    = {3414},
  publisher =	 {Springer-Verlag}
}

@article{RatShe07,
  author    = {Stefan Ratschan and
               Zhikun She},
  title     = {Safety verification of hybrid systems by constraint propagation-based
               abstraction refinement},
  journal   = {ACM Transactions on Embedded Computing Systems},
  volume    = {6},
  number    = {1},
  year      = {2007}
}

@InProceedings{RatShe07-aisc,
  author =       {Stefan Ratschan and Zhikun She},
  title =        {Constraints for Continuous Reachability in the
                  Verification of Hybrid Systems},
  booktitle =    {Proceedings of the 8th International Conference on
                  Artificial Intelligence and Symbolic Computation},
  year =         {2006},
  volume =       4120,
  pages =        {196--210},
  series =       LNCS,
  publisher =    {Springer-Verlag}
}

@Book{Rei90,
  author =	 {Karl R{\"u}diger Reischuk},
  title = 	 {Einf{\"u}hrung in die Komplexit{\"a}tstheorie},
  publisher = 	 {B.G.~Teubner},
  year = 	 1990
}

 @InProceedings{ReyBouLar04,
  author = 	 {Pierre-Alain Reynier, Patricia Bouyer and Fran{\c c}ois Laroussinie},
  title = 	 {Forward Analysis of Timed Automata},
  booktitle = 	 {Proceedings of Winter School on Modelling and Verifying
                  Parallel Processes ({MOVEP})},
  year =         {2004}
}

@InProceedings{Rey72,
  author = 	 {J. Reynolds},
  title = 	 {Definitional Interpreters for Higher-order
                  Programming Languages},
  booktitle = 	 {Proceedings of the 25th ACM National Conference},
  pages =	 {717-740},
  year =	 1972
}

@InProceedings{Rey74,
  author = 	 {J. C. Reynolds},
  title = 	 {Towards a Theory of Type Structure},
  booktitle = 	 {Procedings of Colloque sur la Programmation},
  year =	 1974,
  editor =	 {B. Robinet},
  volume =	 19,
  series =	 {LNCS},
  publisher =    {Springer-Verlag}
}

@InProceedings{Rey85,
  author = 	 {J. C. Reynolds},
  title = 	 {Three Approaches to Type Structure},
  booktitle = 	 {Mathematical Foundations of Software Development},
  year =	 1985,
  volume =	 185,
  series =       {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{Rin98,
  author = 	 {Jussi Rintanen},
  title = 	 {A Planning Algorithm not based on Directional
                  Search},
  booktitle = 	 {Proceedings of the 6th International Conference on
                  Principles of Knowledge Representation and Reasoning},
  pages =	 {617-625},
  year =	 1998,
  editor =	 {Anthony G. Cohn, Lenhard K. Schubert, Stuart C. Shapiro},
  publisher =	 {Morgan Kaufmann}
}

@TechReport{Rin04,
  author = 	 {Jussi Rintanen},
  title = 	 {Introduction to Automated Planning},
  institution =  {Albert-Ludwigs-Universit{\"a}t Freiburg},
  year = 	 2004,
  address =	 {Available from
                  \url{http://www.informatik.uni-freiburg.de/~ki/teaching/ss04/aip/script.pdf}},
  note =	 {Lecture}
}

@inproceedings{RoeHel08,
  author    = {Malte Helmert and
               Gabriele R{\"o}ger},
  title     = {How Good is Almost Perfect?},
  booktitle = {AAAI},
  year      = {2008},
  pages     = {944-949},
  crossref  = {DBLP:conf/aaai/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/aaai/2008,
  editor    = {Dieter Fox and
               Carla P. Gomes},
  title     = {Proceedings of the Twenty-Third AAAI Conference on Artificial
               Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13-17,
               2008},
  booktitle = {AAAI},
  publisher = {AAAI Press},
  year      = {2008},
  isbn      = {978-1-57735-368-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Book{RoeEng,
  author =	 {Roever and Engelhard},
  title = 	 {Data Refinement --- Model-Oriented Proof Methods
and their Comparison},
  publisher = 	 {Publisher},
  year = 	 {}
}

@Book{Roj96,
  author =	 {Ra{\'u}l Rojas},
  title = 	 {Neural Networks. A Systematic Introduction},
  publisher = 	 {Springer-Verlag},
  year = 	 1996
}

@Book{Ros97,
  author =	 {A. W.  Roscoe},
  title = 	 {Theory and Practice of Concurrency},
  publisher = 	 {Prentice Hall},
  year = 	 1997
}

@inproceedings{RozVar07,
  author    = {Kristin Y. Rozier and
               Moshe Y. Vardi},
  title     = {{LTL} Satisfiability Checking},
  booktitle = {SPIN},
  year      = {2007},
  pages     = {149-167},
  ee        = {http://dx.doi.org/10.1007/978-3-540-73370-6_11},
  crossref  = {spin2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{spin2007,
  editor    = {Dragan Bosnacki and
               Stefan Edelkamp},
  title     = {Model Checking Software, 14th International SPIN Workshop,
               Berlin, Germany, July 1-3, 2007, Proceedings},
  booktitle = {SPIN},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4595},
  year      = {2007},
  isbn      = {978-3-540-73369-0},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{RueVal04,
  author = 	 {Camilo Rueda and Frank Valencia},
  title = 	 {Non-Viability Deductions in Arc-Consistency Computation},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Book{RusNor03,
  author =	 {Stuart J. Russell and Peter Norvig},
  title = 	 {Artificial Intelligence: a Modern Approach},
  publisher = 	 {Prentice Hall},
  year = 	 2003,
  series =	 {Series in artificial intelligence},
  annote =	 {2nd ed.}
}

@MastersThesis{Rya04,
  author = 	 {Lawrence Ryan},
  title = 	 {Efficient Algorithms for Clause-Learning {SAT} Solvers},
  school = 	 {Simon Fraser University},
  year = 	 2004
}

@InProceedings{RybSof07,
  author = 	 {Andrey Rybalchenko and Viorica Sofronie-Stokkermans},
  title = 	 {Constraint Solving for Interpolation},
  booktitle = 	 {Proceedings of the 8th International Conference on
Verification, Model Checking and Abstract Interpretation},
  year =	 2007,
  editor =       {Byron Cook and Andreas Podelski},
  volume =       {????},
  series =       {LNCS},
  publisher =    {Springer-Verlag}
}

@inproceedings{Saf88,
  author    = {Shmuel Safra},
  title     = {On the Complexity of omega-Automata},
  booktitle = {FOCS},
  year      = {1988},
  pages     = {319-327},
  crossref  = {FOCS29},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{FOCS29,
  title     = {29th Annual Symposium on Foundations of Computer Science,
               24-26 October 1988, White Plains, New York, USA},
  booktitle = {FOCS},
  publisher = {IEEE},
  year      = {1988},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{SamSchTorSamAzi08,
  author    = {Mehdi Samadi and
               Jonathan Schaeffer and
               Fatemeh Torabi Asr and
               Majid Samar and
               Zohreh Azimifar},
  title     = {Using abstraction in Two-Player Games},
  booktitle = {ECAI},
  year      = {2008},
  pages     = {545-549},
  ee        = {http://dx.doi.org/10.3233/978-1-58603-891-5-545},
  crossref  = {DBLP:conf/ecai/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@MastersThesis{Sch08,
  author = 	 {Alexander Schimpf},
  title = 	 {Implementierung eines {V}erfahrens zur {E}rzeugung von 
                  {B}{\"u}chi-{A}utomaten aus {LTL}-{F}ormeln in {I}sabelle},
  school = 	 {Albert-Ludwigs-Universit{\"a}t Freiburg},
  year = 	 2008,
  type =	 {Diplomarbeit},
  note =         {\url{http://www.informatik.uni-freiburg.de/~ki/papers/diplomarbeiten/schimpf-diplomarbeit-08.pdf}}
}

@InProceedings{SchHof99,
  author = 	 {Klaus Schneider and Dirk W. Hoffmann},
  title = 	 {A {HOL} Conversion for Translating Linear Time Temporal Logic 
                  to {$\omega$}-Automata},
  booktitle = 	 {TPHOLs'99: 12th International Conference on
                  Theorem Proving in Higher Order Logics},
  editor =       {Y. Bertot et al},
  pages =	 {255--272},
  year =	 1999,
  volume =	 1690,
  series =	 {Lecture Notes in Computer Science},
  address =	 {Nice, France},
  publisher =	 {Springer-Verlag}
}

@inproceedings{Sch01,
  author    = {Klaus Schneider},
  title     = {Improving Automata Generation for Linear Temporal Logic
               by Considering the Automaton Hierarchy},
  booktitle = {LPAR},
  year      = {2001},
  pages     = {39-54},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/2250/22500039.htm},
  crossref  = {lpar2001},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{lpar2001,
  editor    = {Robert Nieuwenhuis and
               Andrei Voronkov},
  title     = {Logic for Programming, Artificial Intelligence, and Reasoning,
               8th International Conference, LPAR 2001, Havana, Cuba, December
               3-7, 2001, Proceedings},
  booktitle = {LPAR},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2250},
  year      = {2001},
  isbn      = {3-540-42957-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{SchSer04,
  author = 	 {Tom Schrijvers and Alexander Serebrenik},
  title = 	 {Improving {P}rolog Programs: Refactoring for {P}rolog},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {58-72},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Article{SchSha81,
  author = 	 {Richard Schroeppel and Adi Shamir},
  title = 	 {A $T=O(2^{(n/2)})$, $S=O(2^{(n/4)}) $ Algorithm
                  for Certain {NP}-Complete Problems},
  journal = 	 {SIAM Journal on Computing},
  year = 	 1981,
  volume =	 10,
  number =	 3,
  pages =	 {456-464}
}

@TechReport{Sch95,
  author = 	 {M. I. Schwartzbach},
  title = 	 {Polymorphic Type Inference},
  institution =  {BRICS},
  year = 	 1995,
  address =	 {Department of Computer Science, University of
                  Aarhus},
  note =	 {Lecture Series LS-95-3, viii+24 pp}
}

@INPROCEEDINGS{SF97,
  AUTHOR             = {J.~Schumann and B.~Fischer},
  BOOKTITLE          = {Proceedings of the 12th Conference on 
                        Automated Software Engineering},
  PUBLISHER          = {IEEE Press},
  TITLE              = {{NORA/HAMMR: Making Deduction Based Component retrieval Practical}},
  pages = {246-254},
  YEAR               = {1997}
}

@Book{She69,
  author =	 {Ching Lai Sheng},
  title = 	 {Threshold Logic},
  publisher = 	 {Academic Press},
  year = 	 1969
}

@Article{SheHwa66,
  author = 	 {Sheng, C. L. and Hwa, H. R.},
  title = 	 {Testing and Realization of Threshold Functions by 
                  Successive Higher Ordering of Incremental Weights},
  journal = 	 {IEEE Transactions on Electronic Computers},
  year = 	 1966,
  volume =	 {EC-15},
  number =	 2,
  pages =	 {212-220}
}

@InProceedings{SerMes04,
  author = 	 {Alexander Serebrenik and Fred Mesnard},
  title = 	 {On Termination of Binary CLP Programs },
  booktitle = 	 {Proceedings of 14th Workshop on Logic Programming
                  Environments and 3rd Workshop on Multiparadigm
                  Constraint Programming},
  year =	 2004,
  pages =        {51-66},
  editor =	 {Susana Mu{\~n}oz-Hern{\'a}ndez and Jos{\'e} Manuel G{\'o}mez-Perez
                  and Petra Hofstedt},
  note =	 {Held in conjunction with ICLP04}
}

@Book{Sch86,
  author =	 {A. Schrijver},
  title = 	 {Theory of Linear and Integer Programming},
  publisher = 	 {Wiley},
  year = 	 1986
}

@Article{Sha93,
  author = 	 {U. A. Shankar},
  title = 	 {An Introduction to Assertional Reasoning for
                  Concurrent Systems},
  journal = 	 {ACM Computing Surveys},
  year = 	 1993,
  volume =	 25,
  number =	 3,
  pages =	 {225-262}
}

@InProceedings{SilStuKroEng01,
  author = 	 {B. Silva and O. Stursberg and B. Krogh and B. Engell},
  title = 	 {An Assessment of the Current Status of Algorithmic
                  Approaches to the Verification of Hybrid Systems},
  booktitle = 	 {Proceedings of the IEEE Conference on Decision and Control},
  pages =	 {2867-2874},
  year =	 2001,
  volume =	 3
}

@article{SimNieSoi02,
  author    = {Patrik Simons and
               Ilkka Niemel{\"a} and
               Timo Soininen},
  title     = {Extending and implementing the stable model semantics},
  journal   = {Artificial Intelligence},
  volume    = {138},
  number    = {1-2},
  year      = {2002},
  pages     = {181-234}
}

@Misc{Sloane,
  author =	 {Neil J. A. Sloane},
  title =	 {On-Line Encyclopedia of Integer Sequences},
  howpublished = {\url{http://www.research.att.com/$\sim$njas/sequences/Seis.html}}
}

@Book{Smi06,
  author =	 {Joshua B. Smith},
  title = 	 {Practical OCaml},
  publisher = 	 {Apress},
  year = 	 2006
}

@inproceedings{Sor04,
  author    = {Maria Sorea},
  title     = {Lazy Approximation for Dense Real-Time Systems.},
  booktitle = {Proceedings of the Joint International Conferences on Formal Modelling
               and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques
               in Real-Time and Fault-Tolerant Systems, FTRTFT 2004},
  editor    = {Yassine Lakhnech and
               Sergio Yovine},
  year      = {2004},
  pages     = {363-378},
  publisher = {Springer-Verlag},
  series    = {LNCS}, 
  volume    = {3253},
}


@Article{Sta01,
  author = 	 {Pantelimon St{\v{a}}nic{\v{a}}},
  title = 	 {Coog lower and upper bounds on binomial coefficients},
  journal = 	 {Journal of Inequalities in Pure and Applied Mathematics },
  year = 	 2001,
  volume =	 2,
  number =	 3
}

@InProceedings{Ste06,
  author = 	 {Igor St{\'e}phan}, 
  title = 	 {Boolean Propagation Based on Literals for
Quantified {B}oolean Formulae},
  booktitle = 	 {Proceedings of the 17th European Conference on
                  Artificial Intelligence},
  pages =	 {452-456},
  year =	 2006,
  editor =	 {Gerhard Brewka and Silvia Coradeschi and Anna Perini
                  and Paolo Traverso},
  publisher =	 {IOS Press}
}

@inproceedings{Str00,
  editor    = {E. Allen Emerson and
               A. Prasad Sistla},
  author    = {Ofer Strichman},
  title     = {Tuning {SAT} Checkers for Bounded Model Checking},
  booktitle = {Proceedings of the 12th International Conference on
                  Computer Aided Verification}, 
  year      = {2000},
  volume    = {1855},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  pages     = {480-494}
}

@Article{Str04,
  author = 	 {Ofer Strichman},
  title = 	 {Accelerating Bounded Model Checking of Safety
                  Properties},
  journal = 	 {Formal Methods in System Design},
  year = 	 2004,
  volume =	 24,
  number =	 1,
  pages =	 {5-24}
}

%Hybrid Systems {IV}; sic!
@InProceedings{StuKowHofPre97,
  author = 	 {Olaf Stursberg and Stefan Kowalewski and Ingo
                  Hoffmann and J{\"o}rg Preu{\ss}ig},
  title = 	 {Comparing Timed and Hybrid Automata as
                  Approximations of Continuous Systems},
  booktitle = 	 {Hybrid Systems {IV}},
  pages =	 {361-377},
  year =	 1997,
  editor =	 {Panos J. Antsaklis and Wolf Kohn and Anil Nerode and Shankar Sastry},
  volume =	 1273,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Book{SutBar98,
  author =	 {Richard S. Sutton and Andrew G. Barto},
  title = 	 {Reinforcement Learning},
  publisher = 	 {The MIT Press},
  year = 	 1998
}

@inproceedings{TabVar05,
  editor    = {Geoff Sutcliffe and
               Andrei Voronkov},
  author    = {Deian Tabakov and
               Moshe Y. Vardi},
  title     = {Experimental Evaluation of Classical Automata Constructions},
  booktitle = {Proceedings of the 12th International Conference on 
               Logic for Programming, Artificial Intelligence},
  year      = {2005},
  pages     = {396-411},
  publisher = {Springer-Verlag},
  series    = {LNCS}
}

@Article{Tar55,
  author =       "A. Tarski",
  title =        "A lattice-theoretical fixpoint theorem and its applications",
  journal =      "Pacific J. Math.",
  pages =        "285--309",
  volume =       "5",
  year =         "1955"
}

@article{TauHel02,
  author    = {Heikki Tauriainen and
               Keijo Heljanko},
  title     = {Testing {LTL} formula translation into {B}{\"u}chi automata},
  journal   = {International Journal on Software Tools for Technology Transfer},
  volume    = {4},
  number    = {1},
  year      = {2002},
  pages     = {57-70},
  ee        = {http://link.springer.de/link/service/journals/10009/bibs/2004001/20040057.htm},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{TalTof97,
  author = 	 {M. Tofte and J.-P. Talpin},
  title = 	 {Region-based Memory Management},
  journal = 	 {Information and Computation},
  year = 	 1997,
  volume =	 132,
  number =	 2,
  pages =	 {109-176}
}

@Article{Thi99,
  author = 	 {P. Thiemann},
  title = 	 {Combinators for Program Generation},
  journal = 	 {Journal of Functional Programming},
  year = 	 1999,
  volume =	 9,
  number =	 5,
  pages =	 {483-525}
}

@incollection{Tho90,
  author    = {Wolfgang Thomas},
  title     = {Automata on Infinite Objects},
  booktitle = {Handbook of Theoretical Computer Science, Volume B: Formal
               Models and Sematics (B)},
  year      = {1990},
  pages     = {133-192},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  publisher = {Elsevier and MIT Press}
}

@InCollection{Tho00,
  author = 	 {Wolfgang Thomas},
  title = 	 {Complementation of {B{\"u}chi} Automata Revisited},
  booktitle = 	 {Jewels are forever, Contributions on Theoretical
                  Computer Science in Honor of Arto Salomaa},
  pages =	 {109-122},
  publisher =	 {Springer-Verlag},
  year =	 2000,
  editor =	 {G.~Rozenberg and J.~Karhum{\"a}ki}
}

@Unpublished{Tiw06,
  author = 	 {Ashish Tiwari},
  title = 	 {Abstractions for Hybrid Systems},
  note = 	 {Distilled from \emph{Hybrid Systems: Computation and
                  Control SCC. 2002, 2003, 2004}}
}

%Inbook does not suit my needs
@InProceedings{TorTri01,
  author = 	 {Vetle Ingvald Torvik and
                  E. Trintaphyllou},
  title = 	 {Inference of Monotone {B}oolean Functions},
  booktitle = 	 {Encyclopedia of Optimization},
  pages =	 {472-480},
  year =	 2001,
  editor =	 {Chris A. Floudas and Panos M. Pardalos},
  publisher =	 {Kluwer Academic Publishers}
}

@Book{FloPar01,
  editor =	 {Chris A. Floudas and Panos M. Pardalos},
  title = 	 {Encyclopedia of Optimization},
  publisher = 	 {Kluwer Academic Publishers},
  year = 	 2001
}

@Article{TriSteShaLee12,
  author = 	 {Stavros Tripakis and Christos Stergiou and Chris
                  Shaver and Edward A. Lee},
  title = 	 {A Modular Formal Semantics for Ptolemy},
  journal = 	 {Mathematical Structures in Computer Science},
  year = 	 2012,
  note =	 {Under consideration}
}

@inproceedings{Tru07,
  author    = {Miros{\l}aw Truszczy{\'n}ski},
  title     = {Logic Programming for Knowledge Representation},
  editor    = {Ver{\'o}nica Dahl and
               Ilkka Niemel{\"a}},
  publisher = {Springer-Verlag},
  volume    = {4670},
  series    = {LNCS},
  booktitle = {Proceedings pf the 23rd International Conference on Logic Programming},
  year      = {2007},
  pages     = {76-88}
}

@incollection{Tse83,
  AUTHOR = {G. Tseitin},
  TITLE = {On the complexity of derivation in the propositional calculus},
  YEAR = 1983,
  BOOKTITLE = {Automation of Reasoning vol.~2},
  EDITOR = {J. Siekmann and G. Wrightson},
  PUBLISHER = {Springer-Verlag},
  PAGES = {466-483},
  NOTE = {Reprint of an article from 1968}
 }

@Article{Tse68,
  author = 	 {G. Tseitin},
  title = 	 {On the complexity of derivation in the propositional calculus},
  journal = 	 {Studies in Constructive Mathematics and Logic},
  year = 	 1968,
  volume =	 {Part II},
  pages =	 {115-125},
  note =         {Reprinted in \cite{Tse83}}
}

@article{TuSonBar07,
  author    = {Phan Huy Tu and
               Tran Cao Son and
               Chitta Baral},
  title     = {Reasoning and planning with sensing actions, incomplete
               information, and static causal laws using answer set programming},
  journal   = {Theory and Practice of Logic Programming},
  volume    = {7},
  number    = {4},
  year      = {2007},
  pages     = {377-450}
}

@Book{unicode06,
  author =	 {{\SortNoop{Unicode}}{The Unicode Consortium}},
  title = 	 {The Unicode Standard, Version 5.0},
  publisher = 	 {Addison-Wesley Professional},
  year = 	 2006
}

@InProceedings{VanHeyVer04,
  author = 	 {Davy Van Nieuwenborgh and Stijn Heymans and Dirk Vermeir},
  title = 	 {On Programs with Linearly Ordered Multiple Preferences},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {180-194},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@article{Var91,
  author    = {Moshe Y. Vardi},
  title     = {Verification of Concurrent Programs: The Automata-Theoretic
               Framework},
  journal   = {Annals of Pure and Applied Logic},
  volume    = {51},
  number    = {1-2},
  year      = {1991},
  pages     = {79-98}
}

@inproceedings{VarWol86,
  author    = {Moshe Y. Vardi and
               Pierre Wolper},
  title     = {An Automata-Theoretic Approach to Automatic Program Verification
               (Preliminary Report)},
  booktitle = {Proceedings of the 1st Symposium on Logic in Computer Science},
  year      = {1986},
  pages     = {332-344},
  publisher = {IEEE Computer Society}
}

@Article{VarWol94,
  author = 	 {Moshe Y. Vardi and
                  Pierre Wolper},
  title = 	 {Reasoning about Infinite Computations},
  journal = 	 {Information and Computation},
  year = 	 1994,
  volume =	 115,
  number =	 1,
  pages =	 {1-37}
}

@InProceedings{VenGilDen04,
  author = 	 {Joost Vennekens and David Gilig and Marc Denecker},
  title = 	 {Splitting an Operator},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {195-209},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{VenVerBru04,
  author = 	 {Joost Vennekens and Sofie Verbaeten and Maurice Bruynooghe},
  title = 	 {Logic Programs with Annotated Disjunctions},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {431-445},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@InProceedings{WadBlo89,
  author = 	 {P. Wadler and S. Blott},
  title = 	 {How to Make ad-hoc Polymorphism Less ad-hoc},
  booktitle = 	 {Conference Record of the 16th ACM Symposium on Principles of Programming Languages},
  pages =	 {60-76},
  year =	 1989
}

@InProceedings{Wad90,
  author = 	 {P. Wadler},
  title = 	 {Comprehending Monads},
  booktitle = 	 {Conference on {L}isp and Functional Programming},
  year =	 1990,
  address =	 {Nice, France},
  publisher =	 {ACM}
}

@InProceedings{Wad92,
  author = 	 {P. Wadler},
  title = 	 {The Essence of Functional Programming},
  booktitle = 	 {Conference Record of the 19th Annual Symposium on Principles of Programming Languages},
  pages =	 {1-14},
  year =	 1992,
  series =	 {SIGPLAN-SIGACT},
  publisher =	 {ACM}
}

@InProceedings{WakIno04,
  author = 	 {Toshiko Wakaki and Katsumi Inoue},
  title = 	 {Compiling Prioritized Circumscription into Answer Set
  Programming},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {356-370},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Book{Weg87,
  author =	 {Ingo Wegener},
  title = 	 {The Complexity of {B}oolean Functions},
  publisher = 	 {Wiley \& Sons},
  year = 	 1987,
  address =	 {\url{http://eccc.uni-trier.de/eccc-local/ECCC-Books/wegener\_book\_readme.html}}
}

@Book{Weg87-nohtml,
  author =	 {Ingo Wegener},
  title = 	 {The Complexity of {B}oolean Functions},
  publisher = 	 {Wiley \& Sons},
  year = 	 1987
}

@Book{Weg05,
  author =	 {Ingo Wegener},
  title = 	 {Complexity Theory. Exploring the Limits of Efficient Algorithms},
  publisher = 	 {Springer-Verlag},
  year = 	 2005,
  address =	 {\url{http://www.springerlink.com/content/h6500401p97394n6/}}
}

@inproceedings{WehKupPod08,
  author    = {Martin Wehrle and
               Sebastian Kupferschmid and
               Andreas Podelski},
  title     = {Useless Actions Are Useful},
  booktitle = {ICAPS},
  year      = {2008},
  pages     = {388-395},
  crossref  = {DBLP:conf/aips/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/aips/2008,
  editor    = {Jussi Rintanen and
               Bernhard Nebel and
               J. Christopher Beck and
               Eric A. Hansen},
  title     = {Proceedings of the Eighteenth International Conference on
               Automated Planning and Scheduling, ICAPS 2008, Sydney, Australia,
               September 14-18, 2008},
  booktitle = {ICAPS},
  publisher = {AAAI},
  year      = {2008},
  isbn      = {978-1-57735-386-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{WieHilOss07,
  author    = {Jan Wielemaker and
               Michiel Hildebrand and
               Jacco van Ossenbruggen},
  title     = {{P}rolog as the Fundament for Applications on the Semantic
               Web},
  booktitle = {Proceedings of the ICLP'07 Workshop on Applications of Logic
               Programming to the Web, {S}emantic {W}eb and {S}emantic {W}eb
                  Services},
  editor    = {Axel Polleres and
               David Pearce and
               Stijn Heymans and
               Edna Ruckhaus},
  year      = {2007},
  series    = {CEUR Workshop Proceedings},
  volume    = {287}
}

@Article{WieHuaMei08,
  author = 	 {Wielemaker, Jan and Huang, Zhisheng and 
                  {\SortNoop{Meij}}{van der} Meij, Lourens},
  title = 	 {{SWI}-{P}rolog and the {W}eb},
  journal = 	 {Theory and Practice of Logic Programming},
  year = 	 2008,
  volume =	 8,
  number =	 3,
  pages =	 {363-392}
}

@Book{WinHor87,
  author =	 {Patrick Henry Winston and Berthold Klaus Paul Horn},
  title = 	 {{LISP}},
  publisher = 	 {Addison Wesley},
  year = 	 1987
}

@inproceedings{WitVenMarDenBru06,
  author    = {Johan Wittocx and
               Joost Vennekens and
               Maarten Mari{\"e}n and
               Marc Denecker and
               Maurice Bruynooghe},
  title     = {Predicate Introduction Under Stable and Well-Founded Semantics},
  editor    = {Sandro Etalle and
               Miros{\l}aw Truszczy{\'n}ski},
  booktitle     = {Proceedings of the 22nd International Conference on Logic Programming},
  year      = {2006},
  pages     = {242-256},
  publisher = {Springer-Verlag},
  series    = {LNCS}, 
  volume    = {4079}
}

@InProceedings{YouHou04,
  author = 	 {Jia-Huai You and Guiwen Hou},
  title = 	 {Arc-consistency + Unit Propagation = Lookahead},
  booktitle = 	 {Proceedings of the 20th International Conference on
                  Logic Programming},
  pages =	 {314-328},
  year =	 2004,
  editor =	 {Bart Demoen and Vladimir Lifschitz},
  volume =	 3132,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@inproceedings{Yov98,
  author =    {Sergio Yovine},
  editor    = {Grzegorz Rozenberg and
               Frits W. Vaandrager},
  booktitle     = {Lectures on Embedded Systems, European Educational Forum, School
               on Embedded Systems, Veldhoven, The Netherlands, November 25-29,
               1996},
  title = {Model Checking Timed Automata},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {1494},
  year      = {1998},
  pages = {114-152}
}

@inproceedings{Zha97,
  author    = {Hantao Zhang},
  editor    = {William McCune},
  title     = {{SATO}: An Efficient Propositional Prover},
  booktitle = {Proceedings of the 14th International Conference
               on Automated Deduction},
  year      = {1997},
  pages     = {272-275},
  publisher = {Springer-Verlag},
  series    = {LNCS},
  volume    = {1249}

}

@InProceedings{ZhaMadMosMal01,
  author = 	 {Lintao Zhang and Conor F. Madigan and Matthew
                  W. Moskewicz and Sharad Malik},
  title = 	 {Efficient Conflict Driven Learning in {B}oolean
                  Satisfiability Solver},
  booktitle = 	 {Proceedings of the International Conference on Computer-Aided Design},
  pages =	 {279-285},
  year =	 2001,
  publisher =	 {ACM}
}

@Manual{ICS-man2.0,
  title = 	 {{ICS} Manual (version 2.0)},
  organization = {SRI International},
  address =	 {333 Ravenswood Avenue, Menlo Park, CA 94025, USA, \texttt{ruess@csl.sri.com}}
}

%Old papers from thesis.bib
@Article{AM94,
  author = 	 {K.~R.~Apt and E.~Marchiori},
  title = 	 {Reasoning about {P}rolog Programs: From Modes through Types to Assertions},
  journal = 	 {Formal Aspects of Computing},
  year = 	 1994,
  volume =	 6,
  number =	 {6A},
  pages =	 {743--765}
}

@InProceedings{AMSS94,
  author = 	 {T.~Armstrong and K.~Marriott and P.~Schachte and H.~S{\o}ndergaard},
  title = 	 {Boolean Functions for Dependency Analysis: Algebraic Properties and Efficient Representation},
  booktitle = 	 {Proceedings of the 1st Static Analysis Symposium},
  pages =	 {266--280},
  year =	 1994,
  editor =	 {B.~{Le Charlier}},
  series =	 {LNCS},
  volume =       {864},
  publisher =	 {Springer-Verlag}
}

@Article{AMSS98,
  author = 	 {T.~Armstrong and K.~Marriott and P.~Schachte and H.S{\o}ndergaard},
  title = 	 {Two Classes of {B}oolean Functions for Dependency Analysis},
  journal = 	 {Science of Computer Programming},
  year = 	 1998,
  volume =	 31,
  number =	 1,
  pages =	 {3--45}
}

@article{AP94,
  author = 	 {K.~R.~Apt and A.~Pellegrini},
  title = 	 {On the occur-check free {P}rolog programs},
  journal = 	 {ACM Transactions on Programming Languages and Systems},
  volume =	 16,
  number =	 3,
  year =	 1994,
  pages =	 {687--726}
}

@Article{B93,
  author = 	 {M.~Bezem},
  title = 	 {Strong Termination of Logic Programs},
  journal = 	 {Journal of Logic Programming},
  year = 	 1993,
  volume =	 15,
  number =	 {1 \& 2},
  pages =	 {79--97}
}

@techreport{BCHK98,
	author = {F.~Benoy and M.~Codish and A.~Heaton and A.~M.~King},
	title = {Widening {$Pos$} for {E}fficient and {S}calable {G}roundness {A}nalysis},
	number = {515},
	school = {Computing Laboratory},
	note = {Available at {\tt http://www.cs.ukc.ac.uk/pubs/1997/515/index.html}},
	institution = {University of Kent at Canterbury},
	year = 1997
}

@Article{CBGH97,
  author = 	 {M.~Codish and M.~Bruynooghe and M.~{Garc\'{\i}a de la Banda} and M.~Hermenegildo},
  title = 	 {Exploiting Goal Independence in the Analysis of Logic Programs},
  journal = 	 {Journal of Logic Programming},
  year = 	 1997,
  volume =	 32,
  number =	 3,
  pages =	 {247--261}
}

@inproceedings{CC77,
       author = {P.~Cousot and R.~Cousot},
       title= {Abstract interpretation: {A} unified lattice model for
		static analysis of programs by construction or
		approximation of fixpoints},
       booktitle = {Proceedings of the 4th Symposium on 
                    Principles of Programming Languages},
       year = 1977,
       publisher = {ACM Press},
       pages = {238--252}
}

@inproceedings{CD94,
author = {M.~Codish and B.~Demoen},
title = {Deriving Polymorphic Type Dependencies
for Logic Programs Using Multiple
Incarnations of {${P}rop$}},
booktitle = {Proceedings of the 1st Static Analysis Symposium},
pages = {281--296},
year = 1994,
editor = {B.~{Le Charlier}},
series = {LNCS},
publisher = {Springer-Verlag},
volume    = 864
}

@article{CD95,
author = {M.~Codish and B.~Demoen},
title = {Analyzing Logic Programs using ``{PROP}''-ositional Logic
                  Programs and a {M}agic {W}and},
journal = {Journal of Logic Programming},
year = 1995,
volume = 25,
number = 3,
pages = {249--274}
}

@article{CDY94,
author = {M.~Codish and D.~Dams and E.~Yardeni},
title = {Bottom-up Abstract Interpretation of Logic Programs},
journal = {Theoretical Computer Science},
year = 1994,
volume = 124,
number = 1,
pages = {93--125}
}

@InProceedings{Cod97,
  author = 	 {M.~Codish},
  title = 	 {Efficient Goal Directed Bottom-up Evaluation of Logic Programs},
  booktitle = 	 {Proceedings of the 14th Joint International Conference
                  and Symposium on Logic Programming},
  year =	 1997,
  editor =	 {L.~Naish},
  note = {Presented as poster},
  publisher =	 {MIT Press}
}

@InProceedings{DD98,
  author = 	 {S.~Decorte and D.~{De Schreye}},
  title = 	 {Termination Analysis: 
                  Some Practical Properties of the 
                  Norm and Level Mapping Space},
  booktitle = 	 {Proceedings of the 15th Joint International Conference
                  and Symposium on Logic Programming},
  pages =	 {235-249},
  year =	 1998,
  editor =	 {J.~Jaffar},
  publisher =	 {MIT Press}
}

@InProceedings{DW86,
  author = 	 {S.~K.~Debray and D.~S.~Warren},
  title = 	 {Detection and Optimization of Functional Computations in {P}rolog},
  booktitle = 	 {Proceedings of the 3rd International Conference on Logic Programming},
  pages =	 {490-504},
  year =	 1986,
  editor =	 {E.~Shapiro},
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@Article{EG99,
  author = 	 {S.~Etalle and M.~Gabbrielli},
  title = 	 {Layered Modes},
  journal = 	 {Journal of Logic Programming},
  year = 	 1999,
  volume =       {39},
  pages =        {225--244}
}

@inproceedings{GdW94,
	author = {J.~P.~Gallagher and A.~{de} {Waal}},
	title = {Fast and precise regular approximations of
	logic programs},
	booktitle = {Proceedings of the 11th International Conference on Logic Programming},
        editor = {P.~{Van Hentenryck}},
	pages = {599--613},
	publisher = {MIT Press},
	year = 1994
}

@article{H93,
	author = {F.~Henglein},
	title = {Type Inference with Polymorphic Recursion},
	journal = {ACM Transactions on Programming Languages and Systems},
	volume = 15,
	number = {2},
	year = 1993,
	pages = {253--289},
        publisher = {ACM Press}
}

@Article{HWD92,
  author = 	 {M.~Hermenegildo and R.~Warren and S.~K.~Debray},
  title = 	 {Global Flow Analysis as a Practical Compilation Tool},
  journal = 	 {Journal of Logic Programming},
  year = 	 1992,
  volume =	 13,
  number =	 {1-4},
  pages =	 {349-366}
}

@Article{JB92,
  author = 	 {G.~Janssens and M.~Bruynooghe},
  title = 	 {Deriving Descriptions of Possible Values of Program
                  Variables by Means of Abstract Interpretation},
  journal = 	 {Journal of Logic Programming},
  year = 	 1992,
  volume =	 13,
  number =	 {2 \& 3},
  pages =	 {205--258},
  note =	 {First author name erroneously spelt ``Janssen''}
}

@InProceedings{K96,
  author = 	 {S.~Kahrs},
  editor = {H.~Kuchen and S.~D.~Swierstra},
  title = 	 {Limits of {M}{L}-Definability},
  booktitle = 	 {Proceedings of the 8th Symposium on Programming Language Implementations and Logic Programming},
  pages =	 {17-31},
  year =	 1996,
  series =	 {LNCS},
  volume =       {1140},
  publisher =	 {Springer-Verlag}
}

@article{KTU93-acm,
	author = {A.~J.~Kfoury and J.~Tiuryn and P.~Urzyczyn},
	title = {Type Reconstruction in the Presence of Polymorphic Recursion},
	journal = {ACM Transactions on Programming Languages and Systems},
	volume = 15,
	number = {2},
	year = 1993,
        note = {Title wrongly given in table of contents: 
                Type {\em recursion} in the presence of polymorphic recursion},
	pages = {290--311}
}

@Book{L87,
author = {J.~W.~Lloyd},
title = {Foundations of Logic Programming},
publisher = {Springer-Verlag},
year = 1987
}

@InProceedings{L93,
  author = 	 {S.~L{\"u}ttringhau{s-K}appel},
  title = 	 {Control Generation for Logic Programs},
  booktitle = 	 {Proceedings of the 10th International Conference on Logic Programming},
  pages =	 {478--495},
  year =	 1993,
  editor =	 {D.~S.~Warren},
  publisher =	 {MIT Press}
}

@Article{M78,
  author = 	 {R.~Milner},
  title = 	 {A Theory of Type Polymorphism in Programming},
  journal = 	 {Journal of Computer and System Sciences},
  year = 	 1978,
  volume =	 17,
  number =	 3,
  pages =	 {348--375}
}

@unpublished{M88,
     author = "L.~Meertens",
     title = "First Steps Towards the Theory of Rose Trees",
     note = "CWI, Amsterdam; IFIP Working Group 2.1 working paper 592~ROM-25",
     year = "1988"
}

@InProceedings{MKS96,
  author = 	 {J.~C.~Martin and A.~M.~King and P.~Soper},
  title = 	 {Typed norms for typed logic programs},
  booktitle = 	 {Proceedings of the 6th International Workshop on Logic Program Synthesis and Transformation},
  pages =	 {224--238},
  year =	 1997,
  editor =	 {J.~P.~Gallagher},
  series = {LNCS}, 
  publisher =	 {Springer-Verlag}
}

@article{MO84,
author = {A.~Mycroft and R.~O'Keefe},
title  = {A polymorphic type system for {P}rolog},
journal = {Artificial Intelligence},
year = {1984},
volume = {23},
pages = {295--307}
}

@article{MS93,
	author = {K.~Marriott and H.~S{\o}ndergaard},
	title = {Precise and Efficient Groundness Analysis for Logic Programs},
	journal = {ACM Letters on Programming Languages and Systems},
	volume = 2,
	number = {1--4},
	year = 1993,
	pages = {181--196}
}

@InProceedings{MT95,
  author = 	 {E.~Marchiori and F.~Teusink},
  title = 	 {Proving Termination of Logic Programs with Delay Declarations},
  booktitle = 	 {Proceedings of the 12th International Logic Programming Symposium},
  pages =	 {447--461},
  year =	 1995,
  editor =	 {J.~W.~Lloyd},
  publisher =	 {MIT Press}
}

@TechReport{N92,
  author = 	 {L.~Naish},
  title = 	 {Coroutining and the construction of terminating logic programs},
  institution =  {University of Melbourne},
  year = 	 1992,
  number =	 {92/5}
}

@Book{P92,
  editor =	 {F.~Pfenning},
  title = 	 {Types in Logic Programming},
  publisher = 	 {MIT Press},
  year = 	 1992
}

@TechReport{SGal95,
  author = 	 {H.~Sa\u{g}lam and J.~P.~Gallagher},
  title = 	 {Approximating Constraint Logic Programs Using Polymorphic Types and Regular Descriptions},
  institution =  {University of Bristol},
  year = 	 1995,
  number =	 {CSTR-95-017},
  note =	 {Presented as a poster at the 7th Symposium on Programming Language Implementations and Logic Programming}
}

@Book{T99,
  author =	 {S.~Thompson},
  title = 	 {Haskell: The Craft of Functional Programming},
  publisher = 	 {Addison-Wesley},
  year = 	 1999,
  note =	 {Second Edition}
}

@inproceedings{TL97,
	author = {J.~Tan and I.~Lin},
	title = {Recursive Modes for Precise Analysis of Logic Programs},
	pages = {277--290},
	booktitle = {Proceedings of the 14th International Logic Programming Symposium},
	publisher = {MIT Press},
        editor = {J.~Ma{\l}uszy{\'n}ski},
	year = 1997
}

@Book{Tho91,
  author =	 {S.~Thompson},
  title = 	 {Type Theory and Functional Programming},
  publisher = 	 {Addison-Wesley},
  year = 	 1991
}

@Book{Tho95,
  author =	 {S.~Thompson},
  title = 	 {Miranda: The Craft of Functional Programming },
  publisher = 	 {Addison-Wesley},
  year = 	 1995
}

@article{mercury,
        author =        {Z.~Somogyi and F.~Henderson and T.~Conway},
        title =         {The Execution Algorithm of {Mercury}, an Efficient
                        Purely Declarative Logic Programming Language},
        journal =       {Journal of Logic Programming},
        volume =        {29},
        number =        {1--3},
        pages =         {17--64},
        year =          {1996}
}

%Old papers from modes_types.bib
@Article{CL00,
  author = 	 {M. Codish and V. Lagoon},
  title = 	 {Type Dependencies for Logic Programs using {ACI}-unification},
  journal = 	 {Theoretical Computer Science},
  year = 	 2000,
  volume =	 238,
  number =	 {1--2},
  pages =	 {131--159}
}

@InBook{HT92-new,
  author =	 {P.~M.~Hill and R.~W.~Topor},
  title = 	 {A Semantics for Typed Logic Programs},
  chapter = 	 1,
  pages =	 {1--61},
  year =         1992,
  publisher =    {MIT Press},
  note =	 {In \cite{P92}}
}

@InBook{Han92,
  author =	 {M.~Hanus},
  title = 	 {Logic Programming with Type Specifications},
  chapter = 	 3,
  pages =	 {91--140},
  year =         1992,
  publisher =    {MIT Press},
  note =         {In~\cite{P92}}
}

@InProceedings{LR91,
  author = 	 {T. K.~Lakshman and U. S.~Reddy},
  title = 	 {Typed {P}rolog: A Semantic Reconstruction of the
                  {M}ycroft-{O}'{K}eefe Type System},
  booktitle = 	 {Proceedings of the 1991 International Symposium on
                  Logic Programming},
  pages =	 {202--217},
  year =	 1991,
  editor =	 {V.~Saraswat and K.~Ueda},
  publisher =	 {MIT Press}
}

@InProceedings{LR96,
  author = 	 {P.~Louvet and O.~Ridoux},
  editor = {H.~Kuchen and S.~D.~Swierstra},
  title = 	 {Parametric Polymorphism for {T}yped {P}rolog and $\lambda${P}rolog},
  booktitle = 	 {Proceedings of the 8th Symposium on Programming Language Implementations and Logic Programming},
  pages =	 {47--61},
  year =	 1996,
  series =	 {LNCS},
  volume =       {1140},
  publisher =	 {Springer-Verlag}
}

@InProceedings{LS01,
  author = 	 {V. Lagoon and P. J. Stuckey},
  title = 	 {A Framework for Analysis of Typed Logic Programs},
  booktitle = 	 {Proceedings of the 5th International 
                  Symposium on Functional and Logic Programming},
  year =         2001,
  editor =       {H. Kuchen and K. Ueda},
  series =       {LNCS},
  publisher =    {Springer-Verlag},
  pages =        {296--310},
  volume =       {2024}
}

@InBook{NP92,
  author =	 {G. Nadathur and F. Pfenning},
  title = 	 {Types in Higher-Order Logic Programming},
  chapter = 	 9,
  pages =	 {245--283},
  year =         1992,
  publisher =    {MIT Press},
  note =	 {In \cite{P92}}
}

@InProceedings{Oka97,
  author = 	 {C. Okasaki},
  title = 	 {Catenable Double-Ended Queues},
  booktitle = 	 {Proceedings of the International Conference on Functional Programming},
  pages =	 {66--74},
  year =	 1997,
  volume =	 {32(8)},
  series =	 {{SIGPLAN} Notices },
  publisher =	 {ACM Press}
}

@Book{Pau96,
  author =	 {L. C. Paulson},
  title = 	 {{ML} for the Working Programmer},
  publisher = 	 {Cambridge University Press},
  year = 	 1996
}

%Old papers from class.bib
@article{AB91,
        author = "K.~R. Apt and M. Bezem",
        title = "Acyclic Programs",
        journal = ngc,
        volume = 29,
        number = 3,
        pages = "335-363",
        year = 1991
}

@ARTICLE{AP93r,
    AUTHOR = "K.~R. Apt and D. Pedreschi",
    TITLE = "Reasoning about termination of pure {P}rolog programs",
    JOURNAL = "Information and {C}omputation",
    YEAR = 1993,
        NUMBER = 1,
        VOLUME = 106,
        PAGES  = "109-157"
}

@incollection{AP94m,
        author = "K.~R. Apt and D. Pedreschi",
        title = "Modular Termination Proofs for Logic and Pure {P}rolog Programs",
        booktitle = "Advances in Logic Programming Theory",
    editor = "G. Levi",
        publisher = {Oxford University Press},
        year = "1994",
    pages = "183-229"
        }

@Book{Apt97,
  author =   {K.~R. Apt},
  title =    {From Logic Programming to {P}rolog},
  publisher =    {Prentice Hall},
  year =     1997
}

@article{BCF94,
    author = {A. Bossi and N. Cocco and M. Fabris},
    title = {Norms on Terms and their Use in Proving
                Universal Termination of a Logic Program},
        journal = tcs,
        volume = 124,
        number = 2,
    year = 1994,
    pages = {297-328}
}

@inproceedings{BER99,
        author = {A. Bossi and S. Etalle and S. Rossi},
        title = {Properties of Input-Consuming Derivations},
        editor = {S. Etalle and J.-G. Smaus},
    booktitle = {Proc. of the {ICLP} {W}orkshop on {V}erification of {L}ogic {P}rograms},
        SERIES = entcs,
        volume = "30(1)",
        year =  {1999},
}

@Article{BER02,
  author =   {A. Bossi and S. Etalle and S. Rossi},
  title =    {Properties of Input-Consuming Derivations},
  journal =      tplp,
  year =     {2002},
  volume =   {2},
  number =   {2},
  pages =    {125--154}
}

@InProceedings{BLR92,
  author =      "F. Bronsard and T. K. Lakshman and U. S. Reddy",
  title =       "A Framework of Directionality for Proving
                 Termination of Logic Programs",
  booktitle =    "Proc. of the {J}oint {I}nternational {C}onference
    and {S}ymposium on {L}ogic {P}rogramming",
  year =        1992,
  editor =      "K.~R. Apt",
  publisher =   "MIT Press",
  pages =       "321-335"
}

@book{DM93,
    author = "P. Deransart and J. Ma{\l}uszy{\'n}ski",
    title = "A Grammatical View of Logic Programming",
    publisher = "The MIT Press",
    year = 1993
}

@article{EBC99,
author = "S. Etalle and A. Bossi and N. Cocco",
title = {Termination of well-moded programs},
year = "1999",
Journal = jlp,
volume = "38",
number = "2",
pages = {243-257}
}

@book{HL94,
        author = {P. M. Hill and J. W. Lloyd},
        title = {The {G}{\"o}del Programming Language},
    publisher = "The MIT Press",
    year = 1994
}

@article{KKS97,
  author =       "{M. R. K.} {Krishna Rao} and D. Kapur and R. K. Shyamasundar",
  title =        "Proving Termination of {GHC}
      Programs",
  journal =    {New {G}eneration {C}omputing},
  NUMBER = {3},
  volume = 15,
  pages = {293-338},
  year =         "1997"
}

@ARTICLE{Kow79,
    AUTHOR = "R. A. Kowalski",
    TITLE = "Algorithm = {L}ogic + {C}ontrol ",
    JOURNAL = cacm,
    YEAR = 1979,
    VOLUME = 22,
    NUMBER = 7,
    PAGES = "424-436"
}

@Article{Kri63,
  author = 	 {Saul A. Kripke},
  title = 	 {Semantical Considerations on Modal Logics},
  journal = 	 {Acta Philosophica Fennica},
  year = 	 1963,
  volume =	 16,
  pages =	 {83-94}
}

@InProceedings{LagMesStu03,
  author = 	 {V. Lagoon and F. Mesnard and P.J. Stuckey},
  title = 	 {Termination Analysis with Types Is More Accurate},
  booktitle = 	 {Proceedings of the 19th International Conference on
                  Logic Programming},
  pages =	 {254-268},
  year =	 2003,
  editor =	 {C. Palamidessi},
  volume =	 2916,
  series =	 {LNCS},
  publisher =	 {Springer-Verlag}
}

@article{MT99,
        author = "E. Marchiori and F. Teusink",
    title = "On Termination of Logic Programs
                with Delay Declarations",
    year = "1999",
        volume = "39",
        number = "1-3",
        pages = "95-124",
        journal =  jlp
}

@PhdThesis{Rug99,
  author =   {S.~Ruggieri},
  title =    {Verification and Validation of Logic Programs},
  school =   {Dipartimento di Informatica, Universit{\`a} di Pisa},
  year =     1999
}

@article{RugTCS98,
    AUTHOR = "S. Ruggieri",
    TITLE = "{$\exists$}-Universal Termination of Logic Programs",
    YEAR = 2001,
        journal = tcs,
        volume = 254,
        number = "1-2",
        pages = "273-296"
}

@article{SD94,
        author = "D. {De Schreye} and S. Decorte",
        title = "Termination of Logic Programs: the never-ending story",
        journal = jlp,
        year = 1994,
        volume = {19-20},
        pages = "199-260"
        }

@BOOK{SS86,
        AUTHOR = "L. Sterling and E. Shapiro",
        TITLE = "The Art of {P}rolog",
        PUBLISHER = mp,
        YEAR = 1986
}

@manual{sicstus,
        key = "SICStus",
    title = {{SICS}tus {P}rolog {U}ser's Manual},
    organization = {Swedish Institute of Computer Science},
        note = {{\tt http://www.sics.se/isl/sicstuswww/site/documentation.html}},
    year = 2003
}


%Old papers from cwi.bib
@InCollection{AB99,
  author = 	 {K. R. Apt and M. Bezem},
  title = 	 {Formulas as Programs},
  booktitle = 	 {The Logic Programming Paradigm: A 25 Years Perspective},
  pages =	 {75--107},
  publisher =	 {Springer-Verlag},
  year =	 1999,
  editor =	 {K. R. Apt and V. Marek and M. Truszczynski and D. S. Warren}
}

@Article{ABPS98,
  author = 	 {K. R. Apt and J. Brunekreef and A. Schaerf and V. Partington},
  title = 	 {Alma-0: An Imperative Language that Supports
                  Declarative Programming},
  journal = 	 {ACM Transactions on Programming Languages and Systems},
  year = 	 1998,
  volume =	 20,
  number =	 5,
  pages =	 {1014-1066}
}

@InProceedings{AV02,
  author = 	 {K. R. Apt and C. F. M. Vermeulen},
  title = 	 {First-Order Logic as a Constraint Programming Language},
  booktitle = 	 {Proceedings of the 9th International Conference on
                  Logic for Programming, Artificial Intelligence and Reasoning},
  year =	 2002,
  editor =	 {M. Baaz and A. Voronkov},
  series =	 {LNCS},
  volume =       2514,
  pages =        {19--35},
  publisher =	 {Springer-Verlag}
}

@InProceedings{Apt00a,
  author = 	 {K. R. Apt},
  title = 	 {A Denotational Semantics for First-Order Logic},
  booktitle = 	 {Proceedings of the 1st International Conference
                  on Computational Logic},
  pages =	 {53--69},
  year =	 2000,
  editor =	 {J. Lloyd and others},
  series =	 {LNAI},
  volume =       1861,
  publisher =	 {Springer-Verlag}
}


%%%% additions Stephan

@INPROCEEDINGS(vardi:verification,
   KEY = "Vardi87",
   AUTHOR = "Moshe Vardi",
   TITLE = "Verification of Concurrent Programs: The Automata-Theoretic 
            Framework",
   oRgAnIzAtIoN = "IEEE",
   BOOKTITLE = "Proceedings of the Second Symposium on Logic in Computer 
               Science",
   YEAR = 1987,
   month = jun,
   pages = "167--176")

@Book{fitting:proof,
  author =    {Melvin C. Fitting},
  title =        {Proof Methods for Modal and Intuitionistic Logic},
  publisher =    {D. Reidel},
  year =         1983,
  series =    {Synthese Library: Studies in Epistemology, Logic, Methodology
               and Philosophy of Science},
  address =   {Dordrecht, The Netherlands}
}

@InProceedings{daniele:improved,
  author = 	 {M. Daniele and F. Giunchiglia and M. Vardi},
  title = 	 {Improved Automata Generation for Linear Temporal Logic},
  booktitle = 	 {Computer Aided Verification (CAV'99)},
  pages =	 {249--260},
  year =	 1999,
  volume =	 1633,
  series =	 {Lecture Notes in Computer Science},
  address =	 {Trento, Italy},
  publisher =	 {Springer-Verlag}
}

@INPROCEEDINGS{fritz:buchi,
  AUTHOR = {Fritz, Carsten},
  TITLE = {Constructing {B}{\"u}chi Automata from Linear Temporal Logic Using
   Simulation Relations for Alternating {B}{\"u}chi Automata},
  BOOKTITLE = {8th Intl. Conf. Implementation and Application of Automata
    (CIAA 2003)},
  SERIES = {Lecture Notes in Computer Science},
  EDITOR = {Ibarra, Oscar H. and Dang, Zhe},
  YEAR = 2003,
  VOLUME = 2759,
  PAGES = {35--48},
  ADDRESS = {Santa Barbara, CA, USA}
}

@inproceedings{kupferman:complementation,
  author      =  {O. Kupferman and M.Y. Vardi},
  title       =  {Complementation Constructions for Nondeterministic Automata
                  on Infinite Words},
  booktitle =    {11th Intl. Conf. Tools and Algorithms for the Construction
                  and Analysis of systems (TACAS 2005)},
  editor =	 {Nicolas Halbwachs and Lenore Zuck},
  pages =        {206--221},
  volume =       3440,
  address =	 {Edinburgh, Scotland},
  series    =    {Lecture Notes in Computer Science},
  publisher   =  {Springer-Verlag},
  year        =  {2005}
}

@InProceedings{muller:weak,
  author =       {D.E. Muller and A. Saoudi and P.E. Schupp},
  title =        {Weak alternating automata give a simple explanation of why most
                  temporal and dynamic logics are decidable in exponential time},
  booktitle =    {3rd IEEE Symp. Logic in Computer Science (LICS'88)},
  pages =        {422--427},
  year =         1988,
  publisher =    {IEEE Press},
  address =      {Edinburgh, Scotland}
}

@InProceedings{schneider:HOL-conversion,
  author = 	 {Klaus Schneider and Dirk W. Hoffmann},
  title = 	 {A {HOL} Conversion for Translating Linear Time Temporal Logic 
                  to {$\omega$}-Automata},
  booktitle = 	 {TPHOLs'99: 12th International Conference on
                  Theorem Proving in Higher Order Logics},
  editor =       {Y. Bertot et al},
  pages =	 {255--272},
  year =	 1999,
  volume =	 1690,
  series =	 {Lecture Notes in Computer Science},
  address =	 {Nice, France},
  publisher =	 {Springer-Verlag}
}

@InProceedings{SisVarWol87,
  author = 	 {A.P. Sistla and Moshe Vardi and Pierre Wolper},
  title = 	 {Reasoning about Infinite Computation Paths},
  booktitle = 	 {Proceedings of the 24th IEEE FOCS (1983)},
  pages =	 {185-194},
  year =	 1987
}

@InProceedings{somenzi:efficient,
  author = 	 {Fabio Somenzi and Roderick Bloem},
  title = 	 {Efficient {B{\"u}chi} automata from {LTL} formulae},
  booktitle = 	 {12th Intl. Conf. Computer Aided Verification (CAV 2000)},
  pages =	 {257--263},
  year =	 2000,
  editor =	 {E.A. Emerson and A.P. Sistla},
  volume =	 1633,
  series =	 {Lecture Notes in Computer Science},
  address =	 {Chicago, IL},
  publisher =	 {Springer-Verlag}
}

@techreport{tauriainen:translating,
    author = {H. Tauriainen},
    title = {On Translating Linear Temporal Logic into Alternating and Nondeterministic Automata},
    institution = {Helsinki Univ. of Technology, Lab. Theor. Comp. Sci.},
    month = {December},
    number = {A83},
    pages = {132},
    type = {Research Report},
    address = {Espoo, Finland},
    year = {2003},
}

@mastersthesis{WenzelmannBachelor11,
  author = 	 {Fabian Wenzelmann},
  type =     {Bachelor Thesis},
  title = 	 {{Solving the Threshold Synthesis Problem of Boolean Functions by a Combinatorial Algorithm}},
  school = 	 {Universit{\"a}t Freiburg},
  year = 	 {2011}
}

@mastersthesis{SchillingBachelor11,
  author = 	 {Christian Schilling},
  type =     {Bachelor Thesis},
  title = 	 {{Solving the Threshold Synthesis Problem of Boolean Functions by Translation to Linear Programming}},
  school = 	 {Universit{\"a}t Freiburg},
  year = 	 {2011}
}

@conference{PeledSimeone85,
  title       = {Polynomial-time algorithms for regular set-covering and threshold synthesis},
  author      = {Uri N. Peled and Bruno Simeone},
  year        = {1985},
  booktitle   = {{Discrete Applied Mathematics}},
  volume      = {12},
  pages       = {57-69}
}
@conference{muroga70,
  title       = {Enumeration of Threshold Functions of Eight Variables},
  author      = {Saburo Muroga and Tei??chi Tsuboi and Charles R. Baugh},
  year        = {1970},
  booktitle   = {{IEEE Transactions on Computers}},
  volume      = {C-19},
  pages       = {818-825}
}
@phdthesis{winder62,
  title       = {Threshold Logic},
  author      = {Robert O. Winder},
  year        = {1962},
  school      = {Department of Mathematics, Princeton University},
  address     = {Princeton, U.S.A.}
}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% coding: utf-8-unix
%%% End:
